proposition: Lemma brules_preserve_vars_ok : forall R : rules, brules_preserve_vars R = true <-> rules_preserve_vars R.
proof: Proof. intro. unfold brules_preserve_vars, rules_preserve_vars. rewrite forallb_forall. split_all. rewrite <- brule_preserve_vars_ok'. auto. rewrite brule_preserve_vars_ok. destruct x. auto. Qed.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)