proposition: Lemma P_step_in_list : forall R P l l', one_step_list (P_step R P) l' l -> exists t, exists t', exists l1, exists l2, P_step R P t' t /\ l = l1 ++ t :: l2 /\ l' = l1 ++ t' :: l2.
proof: Proof. intros R P l l' H'; induction H'. exists t2; exists t1; exists (@nil term); exists l; repeat split; trivial. destruct IHH' as [u [u' [l3 [l4 [H1 [H2 H3]]]]]]; subst. exists u; exists u'; exists (t :: l3); exists l4; repeat split; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)