proposition: Lemma split'_aux_eq: forall l l', ((fst(split'_aux l l'))++snd(split'_aux l l')) = l.
proof: Proof. intros; functional induction (split'_aux l l'); trivial. rewrite e1 in IHp; simpl in IHp. now simpl; rewrite IHp. Qed.
imports: Coq(List Wf_nat Recdef Compare_dec Arith Peano_dec Lia RelationClasses Sorting.Sorted Sorting.Permutation) hydras(DecPreOrder DecPreOrder_Instances Sort_spec)