proposition: Lemma WF_Fred : WF (red R) -> WF (red (Frs HF R)).
proof: Proof. intro. eapply WF_incl. eapply red_incl. apply hyp4. eapply Fred_WF. eapply WF_incl. eapply red_incl. apply hyp3. hyp. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)