proposition: Lemma context_in : forall R t1 t2, rwr R t1 t2 -> forall f l l', rwr R (Term f (l ++ t1 :: l')) (Term f (l ++ t2 :: l')).
proof: Proof. intros R t1 t2 H; induction H as [ t1 t2 Step | t1 t2 t3 Trans1 Trans2]. intros f l l'; apply t_step; apply one_step_context_in; trivial. intros f l l'; apply t_trans with (Term f (l ++ t2 :: l')). apply in_context; clear - Trans1; induction l; [left | right]; assumption. apply IHTrans2. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)