variable[LE α][DecidableLE α][Std.IsLinearOrder α][BEq α][LawfulBEq α](l:List α)@[grind]def I(n:α)|[]=>[n]|h::t=>ite (n≤h) (n::h::t) (h::I n t)@[grind]def S:List α→List α|[]=>[]|h::t=>I h<|S t@[grind]def D:List α→Prop|[]|[_]=>True|h::h'::t=>h≤h'∧D (h'::t)def A(n):(D l→D (I n l))∧(n::l).Perm (I n l):=by induction l with|nil=>grind|cons _ t=>cases t<;>grind def T:D (S l)∧l.Perm (S l):=by induction l with|nil=>grind|cons h t=>grind[A (S t) h]