proposition: Lemma red_of_sred_reset : forall t u, Srs.red (srs_of_trs R) t u -> red R (term_of_string t) (term_of_string u).
proof: Proof. intros. Srs.redtac. subst. rewrite !term_of_string_fill. destruct (in_map_elim H). destruct H0. destruct x as [l' r']. unfold srule_of_rule in H1. simpl in H1. inversion H1. rewrite !term_of_string_epi. 3:{ eapply h2. apply H0. } 2:{ ded (h2 _ _ H0). cut (maxvar r' <= maxvar l'). lia. rewrite !maxvar_lmax. apply incl_lmax. apply h1. hyp. } apply red_rule. hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)