fact: Definition brules_preserve_vars (R : rules) := forallb (fun x => ListDec.incl beq_nat (vars (rhs x)) (vars (lhs x))) R.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)