proposition: Lemma rtc_red_of_sred : forall x y, Srs.red R # x y -> red (trs_of_srs R) # (term_of_string x) (term_of_string y).
proof: Proof. intros. elim H; intros. apply rt_step. apply red_of_sred. exact H0. apply rt_refl. eapply rt_trans. apply H1. exact H3. Qed.
imports: CoLoR(LogicUtil RelUtil SN VecUtil ListUtil NatUtil)