proposition: Lemma rules_preserve_vars_incl : forall R S : rules, R [= S -> rules_preserve_vars S -> rules_preserve_vars R.
proof: Proof. fo. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)