proposition: Lemma rwr_apply_subst : forall R t1 t2 sigma, rwr R t1 t2 -> rwr R (apply_subst sigma t1) (apply_subst sigma t2).
proof: Proof. intros R t1 t2 sigma H; induction H as [ | t1 t2 t3 H1 Hrec1 H2]. apply t_step; apply one_step_apply_subst; trivial. apply t_trans with (apply_subst sigma t2); trivial. apply one_step_apply_subst; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)