proposition: Lemma WF_sred_mod_of_WF_red_mod : WF (Srs.red_mod E R) -> WF (red_mod (trs_of_srs E) (trs_of_srs R)).
proof: Proof. intro. rewrite WF_red_mod0; is_unary; preserve_vars. cut (forall s, SN (Srs.red_mod E R) s -> forall t, maxvar t = 0 -> t = term_of_string s -> SN (red_mod0 (trs_of_srs E) (trs_of_srs R)) t). intros. intro t. destruct (eq_nat_dec (maxvar t) 0). 2: apply SN_intro; intros ? []; lia. apply H0 with (string_of_term t). apply H. hyp. rewrite term_of_string_epi. refl. hyp. induction 1; intros. apply SN_intro; intros. assert (h : maxvar y = 0). apply (red_mod0_maxvar (rules_preserve_vars_trs_of_srs E) (rules_preserve_vars_trs_of_srs R) H4). rewrite <- (term_of_string_epi h). apply H1 with (string_of_term y). 3: refl. 2: rewrite (term_of_string_epi h); hyp. rewrite <- (string_of_term_epi x). apply sred_mod_of_red_mod. subst. eapply incl_elim with (R := red_mod0 (trs_of_srs E) (trs_of_srs R)). apply red_mod0_incl_red_mod. hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN VecUtil ListUtil NatUtil)