proposition: Lemma Fred_mod_WF_fin : forall E R, WF (red_mod (Fl E) (Fl R)) -> WF (red_mod E R).
proof: Proof. intros E R. rewrite <- !red_mod_Rules, !Rules_Fl. apply Fred_mod_WF. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)