proposition: Lemma eq_bool_ok : forall t1 t2, match eq_bool t1 t2 with true => t1 = t2 | false => t1<> t2 end.
proof: Proof. fix eq_bool_ok0 1. intro t1; case t1; [intro v1 | intros f1 l1]; (intro t2; case t2; [intro v2 | intros f2 l2]); simpl. generalize (X.eq_bool_ok v1 v2); case (eq_var_bool v1 v2). intros v1_eq_v2; rewrite v1_eq_v2; reflexivity. intros v1_diff_v2 v1_eq_v2; apply v1_diff_v2; injection v1_eq_v2; intro; assumption. discriminate. discriminate. generalize (F.Symb.eq_bool_ok f1 f2); case (eq_symb_bool f1 f2). intros f1_eq_f2; rewrite f1_eq_f2. assert (eq_bool_list_ok : match (fix eq_bool_list (l0 l3 : list term) : bool := match l0 with | nil => match l3 with | nil => true | _ :: _ => false end | t3 :: k1 => match l3 with | nil => false | t4 :: k2 => if eq_bool t3 t4 then eq_bool_list k1 k2 else false end end) l1 l2 with true => l1 = l2 | false => l1 <> l2 end). revert l1 l2; clear - eq_bool_ok0. fix eq_bool_list_ok 1. intro l1; case l1; [idtac | intros t1 k1]; (intro l2; case l2; [idtac | intros t2 k2]). reflexivity. discriminate. discriminate. generalize (eq_bool_ok0 t1 t2); case (eq_bool t1 t2). intro t1_eq_t2; rewrite t1_eq_t2. generalize (eq_bool_list_ok k1 k2); case ((fix eq_bool_list (l0 l3 : list term) : bool := match l0 with | nil => match l3 with | nil => true | _ :: _ => false end | t3 :: k3 => match l3 with | nil => false | t4 :: k4 => if eq_bool t3 t4 then eq_bool_list k3 k4 else false end end) k1 k2). intro k1_eq_k2; rewrite k1_eq_k2; reflexivity. intros k1_diff_k2 tk1_eq_tk2; apply k1_diff_k2; injection tk1_eq_tk2; intro; assumption. intros t1_diff_t2 tk1_eq_tk2; apply t1_diff_t2; injection tk1_eq_tk2; intros; assumption. revert eq_bool_list_ok; case ((fix eq_bool_list (l0 l3 : list term) : bool := match l0 with | nil => match l3 with | nil => true | _ :: _ => false end | t3 :: k1 => match l3 with | nil => false | t4 :: k2 => if eq_bool t3 t4 then eq_bool_list k1 k2 else false end end) l1 l2). intro l1_eq_l2; rewrite l1_eq_l2; reflexivity. intros l1_diff_l2 fl1_eq_fl2; apply l1_diff_l2; injection fl1_eq_fl2; intros; assumption. intros f1_diff_f2 fl1_eq_fl2; apply f1_diff_f2; injection fl1_eq_fl2; intros; assumption. Defined.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)