proposition: Lemma trs_of_srs_reverse_trs : forall R, trs_of_srs (reverse_srs (srs_of_trs R)) = reverse_trs R.
proof: Proof. induction R. refl. simpl. destruct a as [l r]. unfold rule_of_srule. simpl. rewrite IHR. refl. Qed.
imports: CoLoR(Srs ATrs SReverse ATerm_of_String String_of_ATerm AUnary SN LogicUtil AMorphism EqUtil NatUtil ListUtil VecUtil)