proposition: Theorem sortDom_perm : forall ls, Permutation ls (sortDom ls).
proof: Proof. induction ls; intuition idtac; simpl in *. econstructor. eapply Permutation_trans. econstructor. eauto. eapply insertInOrder_perm. Qed.
imports: FCF FCF.PRF Permutation