proposition: Lemma one_step_context_in : forall R t1 t2 f l l', one_step R t1 t2 -> one_step R (Term f (l ++ t1 :: l')) (Term f (l ++ t2 :: l')).
proof: Proof. intros R t1 t2 f l l' H; apply in_context; induction l as [ | t l ]; simpl; [ apply head_step | apply tail_step ]; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)