proposition: Lemma WF_red_rev_eq : WF (red (reverse_trs R)) <-> WF (red R).
proof: Proof. rewrite <- !red_mod_empty. assert (nil = reverse_trs nil). refl. rewrite H. apply WF_red_mod_rev_eq. unfold rules_preserve_vars. simpl. tauto. Qed.
imports: CoLoR(Srs ATrs SReverse ATerm_of_String String_of_ATerm AUnary SN LogicUtil AMorphism EqUtil NatUtil ListUtil VecUtil)