proposition: Lemma sred_mod_of_red_mod : forall t u, red_mod (trs_of_srs E) (trs_of_srs R) t u -> Srs.red_mod E R (string_of_term t) (string_of_term u).
proof: Proof. intros. do 2 destruct H. exists (string_of_term x); split. apply rtc_sred_of_red. hyp. apply sred_of_red. hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN VecUtil ListUtil NatUtil)