proposition: Lemma WF_Fhd_red_mod : WF (hd_red_mod E R) -> WF (hd_red_mod (Frs HF E) (Frs HF R)).
proof: Proof. intro. eapply WF_incl. eapply hd_red_mod_incl. apply hyp2. apply hyp4. eapply Fhd_red_mod_WF. eapply WF_incl. eapply hd_red_mod_incl. apply hyp1. apply hyp3. hyp. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)