proposition: Lemma hyp' : rules_preserve_vars DP.
proof: Proof. apply dp_preserve_vars. exact hyp. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)