proposition: Lemma 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. do 3 destruct H. decomp H. subst x. subst y. rewrite !term_of_string_fill. apply red_rule. change (List.In (rule_of_srule (Srs.mkRule x0 x1)) (trs_of_srs R)). unfold trs_of_srs. apply in_map. exact H0. Qed.
imports: CoLoR(LogicUtil RelUtil SN VecUtil ListUtil NatUtil)