proposition: Lemma th_eq_closure : forall t1 t2 (R : term -> term -> Prop), rwr (rwr R) t1 t2 -> rwr R t1 t2.
proof: Proof. intros t1 t2 R. generalize (th_eq_closure_one_step R); unfold rwr. generalize (trans_clos_is_trans (R := one_step R)). generalize (trans_clos (one_step R)); clear R. intros rwr_R rwr_R_trans rwr_R_step H; induction H as [ | ]; auto. apply rwr_R_trans with y; auto. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)