proposition: Lemma P_step_one_step : forall R P s t, P_step R P s t -> one_step R s t.
proof: Proof. intros R P s t; generalize s; clear s; pattern t; apply term_rec3; clear t. intros v s H; inversion H; subst; apply at_top; trivial. intros f l Hl s H; inversion H as [t' s' Hnf H' | f' lt ls H']; clear H; subst. apply at_top; trivial. apply in_context. generalize ls H'; clear ls H'; induction l as [ | t l]; intros ls H'; inversion H' as [t1 t2 l' H'' | t' l1 l2 H'']; clear H'; subst. apply head_step; apply Hl; trivial; left; trivial. apply tail_step; apply IHl; trivial; intros; apply Hl; trivial; right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)