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