proposition: Lemma WF_sred_mod_of_WF_red_mod : WF (red_mod E R) -> WF (Srs.red_mod (srs_of_trs E) (srs_of_trs R)).
proof: Proof. intros H. cut (forall t, SN (red_mod E R) t -> forall s, t = term_of_string s -> SN (Srs.red_mod (srs_of_trs E) (srs_of_trs R)) s). intros. intro s. apply H0 with (term_of_string s). apply H. refl. induction 1. intros. subst. apply SN_intro; intros. apply H1 with (term_of_string y). apply red_mod_of_sred_mod. hyp. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)