proposition: Lemma sred_of_red : forall t u, red R t u -> Srs.red (srs_of_trs R) (string_of_term t) (string_of_term u).
proof: Proof. intros. rewrite (red1_ok is_unary_sig hR) in H. destruct H. decomp H. rewrite H0; clear H0. rewrite H3; clear H3. rewrite !string_of_term_fill, !string_of_cont_comp, !string_of_cont_cont. simpl. rewrite <- !app_nil_end. set (c := SContext.mkContext (string_of_cont x1) (string_of_cont x2)). change (Srs.red (srs_of_trs R) (SContext.fill c (string_of_term x)) (SContext.fill c (string_of_term x0))). apply Srs.red_rule. clear c. change (List.In (srule_of_rule (mkRule x x0)) (srs_of_trs R)). apply in_map. hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)