proposition: Lemma eq_bool_ok : forall vt1 vt2, match eq_bool vt1 vt2 with true => vt1 = vt2 | false => vt1 <> vt2 end.
proof: Proof. intros [v1 t1] [v2 t2]; generalize (X.eq_bool_ok v1 v2) (T.eq_bool_ok t1 t2). unfold eq_bool; case (eq_var_bool v1 v2). case (T1.eq_bool t1 t2). intros; subst; simpl; reflexivity. intros _ t1_diff_t2; simpl; intro vt1_eq_vt2; apply t1_diff_t2; injection vt1_eq_vt2; intros; subst; reflexivity. intros v1_diff_v2 _; simpl; intro vt1_eq_vt2; apply v1_diff_v2; injection vt1_eq_vt2; intros; subst; reflexivity. Defined.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)