proposition: Lemma Rules_Fl : forall R, of_list (Fl R) [=] Frs (of_list R).
proof: Proof. induction R; simpl; intros. fo. rewrite !of_cons, IHR. unfold Frs. rewrite image_add. refl. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)