proposition: Lemma rules_preserve_vars_trs_of_srs : forall R, rules_preserve_vars (trs_of_srs R).
proof: Proof. unfold rules_preserve_vars. induction R; simpl; intuition. unfold rule_of_srule in H0. destruct a. simpl in H0. inversion H0. rewrite !vars_var; is_unary. rewrite !var_term_of_string. unfold incl; simpl; intuition. Qed.
imports: CoLoR(LogicUtil RelUtil SN VecUtil ListUtil NatUtil)