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