proposition: Lemma dp_preserve_vars : rules_preserve_vars dp.
proof: Proof. unfold rules_preserve_vars. intros. destruct (dp_elim_vars H). intuition. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)