proposition: Lemma rules_preserve_vars_reverse_trs : forall R, rules_preserve_vars R -> rules_preserve_vars (reverse_trs R).
proof: Proof. induction R; intros. unfold rules_preserve_vars. simpl. tauto. simpl. revert H. rewrite !rules_preserve_vars_cons. destruct a as [l r]. simpl. intuition. rewrite !vars_var; try (hyp||apply is_unary_sig'). rewrite !var_reverse_term. intuition. Qed.
imports: CoLoR(Srs ATrs SReverse ATerm_of_String String_of_ATerm AUnary SN LogicUtil AMorphism EqUtil NatUtil ListUtil VecUtil)