proposition: Lemma hd_red_mod_reset_eq : hd_red_mod E R == hd_red_mod (reset_rules E) (reset_rules R).
proof: Proof. unfold hd_red_mod. rewrite <- hd_red_reset_eq; try hyp. rewrite <- red_reset_eq; try hyp. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)