proposition: Theorem o_total : forall t1 t2 : term, {o t1 t2} + {o t2 t1}.
proof: Proof. unfold o; apply term_rec7 with (P2:= fun t1 t2 => {o_bool t1 t2 = true} + {o_bool t2 t1 = true}) (Pl2 := fun l1 l2 => {o_term_list l1 l2 = true} + {o_term_list l2 l1 = true}). intros x1 t2; destruct t2 as [x2 | f2 l2]; simpl. destruct (OX1.o_total x1 x2) as [x1_le_x2 | x2_le_x1]; [left | right]. generalize (OX1.o_bool_ok x1 x2); case (OX1.o_bool x1 x2). intros _; reflexivity. intro x1_not_le_x2; absurd (OX1.o x1 x2); assumption. generalize (OX1.o_bool_ok x2 x1); case (OX1.o_bool x2 x1). intros _; reflexivity. intro x2_not_le_x1; absurd (OX1.o x2 x1); assumption. right; reflexivity. intros t1 x2; destruct t1 as [ x1 | f1 l1]. destruct (OX.o_total x1 x2) as [o_x1_x2 | o_x2_x1]; [left | right]. simpl; generalize (OX1.o_bool_ok x1 x2); case (OX1.o_bool x1 x2). intros _; reflexivity. intro x1_not_le_x2; absurd (OX1.o x1 x2); assumption. simpl; generalize (OX1.o_bool_ok x2 x1); case (OX1.o_bool x2 x1). intros _; reflexivity. intro x2_not_le_x1; absurd (OX1.o x2 x1); assumption. simpl; left; reflexivity. intros f1 f2 l1 l2 Hrec; 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]). elim Hrec; intro o_l1_l2; [ left | right ]; trivial. absurd (f2 = f1); auto. absurd (f1 = f2); auto. destruct (OF.o_total f1 f2) as [f1_le_f2 | f2_le_f1]; [left | right]. generalize (OF.o_bool_ok f1 f2); case (OF.o_bool f1 f2). intros _; reflexivity. intro f1_not_le_f2; absurd (OF.o f1 f2); assumption. generalize (OF.o_bool_ok f2 f1); case (OF.o_bool f2 f1). intros _; reflexivity. intro f2_not_le_f1; absurd (OF.o f2 f1); assumption. intro l1; induction l1 as [ | a1 l1]. destruct l2 as [ | a2 l2 ] ; [left | right]; simpl; trivial. destruct l2 as [ | a2 l2 ]. left; simpl; trivial. intro 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]). apply IHl1; intros; apply Hrec; right; trivial. absurd (a2 = a1); auto. absurd (a1 = a2); auto. apply Hrec; left; trivial. Qed.
imports: Coq(Relations List) CoLoR(list_sort term_spec)