proposition: Lemma srs_of_trs_reset : forall R, srs_of_trs (reset_rules R) = srs_of_trs R.
proof: Proof. unfold srs_of_trs, reset_rules. induction R; simpl; intros. refl. rewrite IHR, srule_of_rule_reset. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)