proposition: Lemma rtc_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. induction 1. apply rt_step. apply red_of_sred. hyp. apply rt_refl. apply rt_trans with (term_of_string y); hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)