proposition: Lemma R_in_rwr_R : forall t1 t2 (R : term -> term -> Prop), R t1 t2 -> rwr R t1 t2.
proof: Proof. intros t1 t2 R H; apply t_step; apply at_top; generalize (instance R t1 t2 nil H); do 2 rewrite empty_subst_is_id; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)