proposition: Lemma W12' : well_founded (rdp_step (axiom (ddp (@union _ R1 R2))) (@union _ (@union _ R1 R2) (Pi pi V0 V1))).
proof: Proof. assert (W2' := dp_necessary _ R12_var' W2). refine (wf_incl _ _ _ _ W2'). clear; intros s t H; inversion H; clear H; subst. apply Rdp_step with l2; trivial. inversion H1; clear H1; subst. apply instance. apply dp_incl with (@union _ R1 R2). do 3 intro; left; assumption. apply ddp_is_dp; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)