mathlib3

c851e4e3 - destutter preserves list.edist needs induction over the length of the list, since the cases we induct over are not structural sublists