proposition: Lemma one_step_one_rule : forall R s t, one_step R t s -> exists r, exists l, R r l /\ one_step (fun r' l' => In (r',l') ((r,l) :: nil)) t s.
proof: Proof. intros R s; pattern s; apply term_rec3; clear s. intros v t K; inversion K; subst. inversion H; subst. destruct t2 as [x2 | f2 l2]. exists t1; exists (Var x2); split; [assumption | apply at_top; apply instance; left; apply eq_refl]. discriminate. intros f l IH t K; inversion K; subst. inversion H; subst. exists t1; exists t2; split; trivial. left; apply instance; left; apply eq_refl. destruct (one_step_in_list H1) as [u [u' [k1 [k2 [H2 [H3 H4]]]]]]. assert (u_in_l : In u l). subst; apply in_or_app; right; left; apply eq_refl. destruct (IH u u_in_l u' H2) as [t1 [t2 [K1 K2]]]. exists t1; exists t2; split; trivial. apply in_context. clear IH K H1 u_in_l; subst l l1; induction k1 as [ | a1 k1]. left; assumption. right; apply IHk1; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)