proposition: Lemma brules_preserve_vars_ok : forall R, brules_preserve_vars R = true <-> rules_preserve_vars R.
proof: Proof. intro R. unfold rules_preserve_vars, brules_preserve_vars. rewrite forallb_forall. split. intros h l r hlr. rewrite <- ListDec.incl_ok, <- (h _ hlr). refl. apply beq_nat_ok. intros h [l r] hlr. rewrite ListDec.incl_ok. apply h. hyp. apply beq_nat_ok. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)