proposition: Lemma srule_of_rule_reset : forall a, srule_of_rule (reset_rule a) = srule_of_rule a.
proof: Proof. intros [l r]. unfold srule_of_rule, reset_rule. simpl. rewrite !string_of_term_reset. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)