proposition: Lemma P_step_context_in : forall R P t1 t2 f l l', P_step R P t1 t2 -> P_step R P (Term f (l ++ t1 :: l')) (Term f (l ++ t2 :: l')).
proof: Proof. intros R P t1 t2 f l l' H; apply P_in_context; induction l as [ | t l ]; simpl; [ left | right ]; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)