proposition: Lemma P_general_context : forall R P f l1 l2, trans_clos (one_step_list (P_step R P)) l1 l2 -> trans_clos (P_step R P) (Term f l1) (Term f l2).
proof: Proof. intros R P f l1 l2 H; induction H as [l1 l2 H | l1 l2 l3 H1 H2 H3]. left; right; assumption. right with (Term f l2); trivial. right; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)