proposition: Lemma red_mod_of_sred_mod : forall x y, Srs.red_mod E R x y -> red_mod (trs_of_srs E) (trs_of_srs R) (term_of_string x) (term_of_string y).
proof: Proof. intros. do 2 destruct H. exists (term_of_string x0). split. apply rtc_red_of_sred. exact H. apply red_of_sred. exact H0. Qed.
imports: CoLoR(LogicUtil RelUtil SN VecUtil ListUtil NatUtil)