proposition: Theorem o_anti_sym : forall t1 t2, o t1 t2 -> o t2 t1 -> t1 = t2.
proof: Proof. elim OX.o_proof; intros Rv Tv Av; elim OF.o_proof; intros Rs Ts As; apply (term_rec7 (fun t1 t2 => o t1 t2 -> o t2 t1 -> t1 = t2) (fun l1 l2 => o_term_list l1 l2 = true -> o_term_list l2 l1 = true -> l1 = l2)). intros x1; destruct t2 as [ x2 | f2 l2 ]. unfold o; simpl; intros H1 H2. generalize (OX1.o_bool_ok x1 x2); rewrite H1; clear H1; intro H1. generalize (OX1.o_bool_ok x2 x1); rewrite H2; clear H2; intro H2. rewrite (Av x1 x2 H1 H2); trivial. intros; discriminate. intros t1 x2; destruct t1 as [ x1 | f1 l1 ]. unfold o; simpl; intros H1 H2. generalize (OX1.o_bool_ok x1 x2); rewrite H1; clear H1; intro H1. generalize (OX1.o_bool_ok x2 x1); rewrite H2; clear H2; intro H2. rewrite (Av x1 x2 H1 H2); trivial. intros; discriminate. intros f1 f2 l1 l2 Hrec; simpl. unfold o; simpl; generalize (F.Symb.eq_bool_ok f1 f2); case (F.Symb.eq_bool f1 f2); [intro f1_eq_f2 | intro f1_diff_f2]; (generalize (F.Symb.eq_bool_ok f2 f1); case (F.Symb.eq_bool f2 f1); [intro f2_eq_f1 | intro f2_diff_f1]). intros H1 H2; subst f1; rewrite (Hrec H1 H2); trivial. absurd (f2 =f1); auto. absurd (f1 =f2); auto. intros H1 H2; absurd (f1 = f2); trivial; apply As. generalize (OF1.o_bool_ok f1 f2); rewrite H1; intro; assumption. generalize (OF1.o_bool_ok f2 f1); rewrite H2; intro; assumption. fix o_anti_sym 1; intro l1; case l1; clear l1; [idtac | intros a1 l1]. intros l2 _; case l2; clear l2; [trivial | intros a2 l2]; intros; discriminate. intros l2; case l2; clear l2; [intros; discriminate | intros a2 l2 Hrec; simpl]. generalize (T1.eq_bool_ok a1 a2); case (T1.eq_bool a1 a2); [intro a1_eq_a2 | intro a1_diff_a2]; (generalize (T1.eq_bool_ok a2 a1); case (T1.eq_bool a2 a1); [intro a2_eq_a1 | intro a2_diff_a1]). intros; apply f_equal2; [assumption | apply o_anti_sym; trivial]. intros; apply Hrec; trivial; right; assumption. absurd (a2 = a1); subst; trivial. absurd (a1 = a2); subst; trivial. intros H3 H4; absurd (a1 = a2); trivial. apply Hrec; trivial; left; trivial. Qed.
imports: Coq(Relations List) CoLoR(list_sort term_spec)