fact: Hypothesis split_permutation: forall l, Permutation ((fst(split l))++snd(split l)) l.
imports: Coq(List Wf_nat Recdef Compare_dec Arith Peano_dec Lia RelationClasses Sorting.Sorted Sorting.Permutation) hydras(DecPreOrder DecPreOrder_Instances Sort_spec)