proposition: Lemma WF_red_mod : WF (Srs.red_mod E R) <-> WF (red_mod (trs_of_srs E) (trs_of_srs 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 VecUtil ListUtil NatUtil)