proposition: Lemma rules_preserve_vars_cons : forall a R, rules_preserve_vars (a :: R) <-> vars (rhs a) [= vars (lhs a) /\ rules_preserve_vars R.
proof: Proof. unfold rules_preserve_vars. split_all. apply H. left. destruct a. refl. fo. simpl in H0. destruct H0. subst. hyp. apply H1. hyp. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)