proposition: Lemma modular_var : forall v, Acc (ddp_step (@union term (@union term R1 R2) (@union _ R3 (Pi pi V0 V1)))) (Var v).
proof: Proof. intro x; apply Acc_intro; intros s H; inversion H; subst. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)