proposition: Lemma Fred_WF_fin : forall R, WF (red (Fl R)) -> WF (red R).
proof: Proof. intro. rewrite <- !red_Rules, Rules_Fl. apply Fred_WF. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)