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