proposition: Lemma rtc_sred_of_red : forall t u, red (trs_of_srs R) # t u -> Srs.red R # (string_of_term t) (string_of_term u).
proof: Proof. induction 1. apply rt_step. apply sred_of_red. hyp. apply rt_refl. apply rt_trans with (string_of_term y); hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN VecUtil ListUtil NatUtil)