proposition: Lemma rwr_inv : forall A R (eq : A -> A -> Prop) (f : term -> A), (forall a1 a2 a3, eq a1 a2 -> eq a2 a3 -> eq a1 a3) -> (forall t1 t2, one_step R t1 t2 -> eq (f t1) (f t2)) -> forall t1 t2, rwr R t1 t2 -> eq (f t1) (f t2).
proof: Proof. intros A R eq f eq_trans Step_inv t1 t2 H; induction H; auto. apply eq_trans with (f y); auto. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)