proposition: Lemma WF_red_mod : WF (red_mod E R) <-> WF (Srs.red_mod (srs_of_trs E) (srs_of_trs R)).
proof: Proof. split; intro. apply WF_sred_mod_of_WF_red_mod. hyp. apply WF_red_mod_of_WF_sred_mod. hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)