proposition: Lemma mdp_criterion_strong : forall (dpR : relation term), (forall u v, dpR v u -> dp R v u) -> well_founded (rest (acc_sub R) (rdp_step (axiom (mrel dpR)) R)) -> well_founded (rest (acc_sub R) (rdp_step (axiom dpR) R)).
proof: Proof. intros dpR dpR_in_dpR W t; apply mdp_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)