proposition: Lemma reverse_trs_reset_rules : forall R, reverse_trs (reset_rules R) = reset_rules (reverse_trs R).
proof: Proof. induction R. refl. simpl. destruct a as [l r]. simpl. rewrite !reverse_term_reset, IHR. unfold reset_rule. simpl. rewrite !reset_reverse_term. refl. Qed.
imports: CoLoR(Srs ATrs SReverse ATerm_of_String String_of_ATerm AUnary SN LogicUtil AMorphism EqUtil NatUtil ListUtil VecUtil)