proposition: Lemma eq_term_dec2 : forall (s12 t12 : term * term), {s12 = t12}+{s12 <> t12}.
proof: Proof. intros [s1 s2] [t1 t2]. generalize (T.eq_bool_ok s1 t1); case (T.eq_bool s1 t1); [intro s1_eq_t1 | intro s1_diff_t1]. generalize (T.eq_bool_ok s2 t2); case (T.eq_bool s2 t2); [intro s2_eq_t2 | intro s2_diff_t2]. left; apply f_equal2; assumption. right; intro s12_eq_t12; apply s2_diff_t2; injection s12_eq_t12; intros s2_eq_t2 _; assumption. right; intro s12_eq_t12; apply s1_diff_t1; injection s12_eq_t12; intros _ s1_eq_t1; assumption. Defined.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)