proposition: Lemma red_mod_of_sred_mod : forall t u, Srs.red_mod (srs_of_trs E) (srs_of_trs R) t u -> red_mod E R (term_of_string t) (term_of_string u).
proof: Proof. intros. do 2 destruct H. exists (term_of_string x); split. apply rtc_red_of_sred; hyp. apply red_of_sred; hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)