proposition: Lemma general_context : forall R f l1 l2, rwr_list (one_step R) l1 l2 -> rwr R (Term f l1) (Term f l2).
proof: Proof. intros R f l1 l2 H; induction H as [l1 l2 H | l1 l2 l3 H1 H2]. left; right; assumption. right with (Term f l2); trivial. right; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)