proposition: Lemma rules_preserve_vars_var : forall l r, In (mkRule l r) R -> var r = var l.
proof: Proof. intros. ded (hR _ _ H). rewrite !vars_var in H0. unfold incl in H0. ded (H0 (var r)). simpl in H1. fo. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)