proposition: Lemma 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. intros. redtac. subst. rewrite !string_of_term_fill, !string_of_term_sub, (rules_preserve_vars_var is_unary_sig (rules_preserve_vars_trs_of_srs R) lr). set (c' := mkContext (string_of_cont c) (string_of_term (s (var l)))). change (Srs.red R (SContext.fill c' (string_of_term l)) (SContext.fill c' (string_of_term r))). apply Srs.red_rule. clear c'. destruct (in_map_elim lr). destruct H. destruct x. unfold rule_of_srule in H0. simpl in H0. inversion H0. rewrite !string_of_term_epi. hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN VecUtil ListUtil NatUtil)