proposition: Lemma sred_mod_of_red_mod : forall x y, red_mod E R x y -> Srs.red_mod (srs_of_trs E) (srs_of_trs R) (string_of_term x) (string_of_term y).
proof: Proof. intros. do 2 destruct H. exists (string_of_term x0). split. apply (rtc_sred_of_red hE). hyp. apply (sred_of_red hR). hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)