proposition: Lemma var_cond : forall R : rules, ~rules_preserve_vars R -> EIS (red R).
proof: Proof. intros. rewrite <- red_mod_empty. apply var_cond_mod. hyp. Qed.
imports: CoLoR(LogicUtil ATrs AVariables BoolUtil EqUtil ListUtil RelUtil NatUtil APosition)