proposition: Lemma wf_interp_acc : forall S1, @inclusion _ S1 R1 -> well_founded (rdp_step (axiom (ddp S1)) (@union _ R1 (Pi pi V0 V1))) -> forall s, Interp_dom R1 R2 s -> Acc (rdp_step (axiom (ddp S1)) (@union _ R1 R2)) s.
proof: Proof. intros S1 S1_in_R1 wf s Is. destruct (interp_defined _ Is) as [s' Hs']. apply acc_interp_acc with s'; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)