proposition: Lemma rdp_step_rmdp_step : forall (dpR : relation term), (forall u v, dpR v u -> dp R v u) -> forall s t, rdp_step (axiom dpR) R s t -> rdp_step (axiom (mrel dpR)) R (mark_term s) (mark_term t).
proof: Proof. intros dpR dpR_in_dpR s t H. inversion H as [f l1 l2 _s H1 H2 H3 H4]; clear H; subst. simpl; apply Rdp_step with l2; trivial. inversion H2 as [v u sigma K1 K2 K3]; clear H2; subst; trivial. assert (K1' := dpR_in_dpR _ _ K1); inversion K1' as [t1 t2 p f2 k2 H Sub Df2]; clear K1'; subst. destruct u as [xu | fu lu]. apply False_rect; apply (R_var _ _ H). injection K3; clear K3; intros; subst. apply (instance (mrel dpR) (Term (mark f2) k2) (Term (mark f) lu) sigma). apply (Mrel dpR (Term f2 k2) (Term f lu)). assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)