proposition: Lemma mdp_strong_necessary_local : (forall f, mark (mark f) = f) -> forall (dpR : relation term), (forall u v, dpR v u -> dp R v u) -> well_founded (rest (acc_sub R) (rdp_step (axiom dpR) R)) -> well_founded (rest (acc_sub R) (rdp_step (axiom (mrel dpR)) R)).
proof: Proof. intros mark_inv dpR dpR_in_dpR W. intro t; rewrite (TT mark_inv t). apply mdp_reverted_criterion_local_strong; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)