proposition: Lemma WF_Fred_iso : WF (red R) <-> WF (red (Frs HF R)).
proof: Proof. split; intro. apply WF_Fred with (G:=G) (HG:=HG) (R':=Frs HF R). apply Frs_epi. refl. hyp. apply Fred_WF with (S2:=S2) (F:=F) (HF:=HF). hyp. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)