proposition: Lemma rules_preserve_vars_reset : rules_preserve_vars (reset_rules R).
proof: Proof. intros l0 r0 h. destruct (in_map_elim h). destruct H. destruct x as [l r]. unfold reset_rule in H0. simpl in H0. inversion H0. rewrite !vars_var, !var_reset. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)