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