proposition: Lemma maxvar_reset_rules : forall R a, In a (reset_rules R) -> maxvar (lhs a) = 0 /\ maxvar (rhs a) = 0.
proof: Proof. intros. unfold reset_rules in H. destruct (in_map_elim H). destruct H0. subst. destruct x as [l r]. unfold reset_rule. simpl. rewrite !maxvar_reset. auto. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)