proposition: Lemma mrdp_step_rdp_step : (forall f, mark (mark f) = f) -> forall (dpR : relation term), (forall u v, dpR v u -> dp R v u) -> forall s t, rdp_step (axiom (mrel dpR)) R (mark_term s) (mark_term t) -> rdp_step (axiom dpR) R s t.
proof: Proof. intros mark_inv dpR dpR_in_dpR. intros s t H. inversion H as [_f l1 l2 _s H1 H2 H3 H4]; clear H; subst. destruct t as [ | f l1']; [discriminate | injection H4; clear H4; intros; subst _f l1']. simpl; apply Rdp_step with l2; trivial. inversion H2 as [_v _u sigma _K1 K2 K3]; clear H2; subst; trivial. inversion _K1 as [v u K1]; clear _K1; subst. 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. assert (_K2 := f_equal mark_term K2); simpl in _K2; rewrite <- (TT mark_inv) in _K2; rewrite mark_inv in _K2. rewrite <- _K2. apply (instance dpR (Term f2 k2) (Term f lu) sigma). assert (_H2 := f_equal mark H2); do 2 rewrite mark_inv in _H2. subst f; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)