proposition: Lemma red_of_sred : forall t u, Srs.red (srs_of_trs R) t u -> red R (term_of_string t) (term_of_string u).
proof: Proof. intros. rewrite red_reset. apply red_of_sred_reset. apply rules_preserve_vars_reset. hyp. intros. destruct (in_map_elim H0). destruct H1. unfold reset_rule in H2. inversion H2. rewrite maxvar_var. rewrite var_reset. refl. hyp. hyp. rewrite srs_of_trs_reset. hyp. hyp. hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)