proposition: Theorem insertInOrder_twice_eq : forall (ls : list (A * B)) a1 b1 a2 b2, a1 <> a2 -> insertInOrder (insertInOrder ls a1 b1) a2 b2 = insertInOrder (insertInOrder ls a2 b2) a1 b1.
proof: Proof. induction ls; intuition idtac; simpl in *. case_eq (leA a2 a1); intros. case_eq (leA a1 a2); intros. exfalso. eapply H. eapply leA_antisymm; eauto. trivial. case_eq (leA a1 a2); intros. trivial. specialize (leA_total a1 a2). rewrite H0 in leA_total. rewrite H1 in leA_total. discriminate. case_eq (leA a1 a0); intros; case_eq (leA a2 a0); intros. simpl. case_eq (leA a2 a1); intros; case_eq (leA a1 a2); intros. exfalso. eapply H. eapply leA_antisymm; eauto. rewrite H0. trivial. rewrite H1. trivial. specialize (leA_total a1 a2). rewrite H2 in leA_total. rewrite H3 in leA_total. discriminate. simpl. rewrite H0. case_eq (leA a2 a1); intros. erewrite leA_trans in H1; eauto. discriminate. rewrite H1. trivial. simpl. rewrite H1. rewrite H0. case_eq (leA a1 a2); intros. erewrite leA_trans in H0; eauto. discriminate. trivial. simpl. rewrite H1. rewrite H0. f_equal. eauto. Qed.
imports: FCF FCF.PRF Permutation