proposition: Lemma red_mod_reset : forall t u, red_mod E R t u <-> red_mod (reset_rules E) (reset_rules R) t u.
proof: Proof. rewrite <- rel_eq. apply red_mod_reset_eq. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)