proposition: Lemma P_context_in : forall R P t1 t2, trans_clos (P_step R P) t1 t2 -> forall f l l', trans_clos (P_step R P) (Term f (l ++ t1 :: l')) (Term f (l ++ t2 :: l')).
proof: Proof. intros R P t1 t2 H; induction H as [ t1 t2 Step | t1 t2 t3 Trans1 Trans2]. intros f l l'; apply t_step; apply P_step_context_in; trivial. intros f l l'; apply trans_clos_is_trans with (Term f (l ++ t2 :: l')); trivial. apply t_step; apply P_step_context_in; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)