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