proposition: Theorem insertInOrder_perm : forall s a b, Permutation ((a, b)::s) (insertInOrder s a b).
proof: Proof. induction s; intuition idtac; simpl in *. eapply Permutation_refl. case_eq (leA a a0); intros. eapply Permutation_refl. eapply Permutation_trans. 2:{ econstructor. eapply IHs. } econstructor. Qed.
imports: FCF FCF.PRF Permutation