proposition: Lemma Frs_epi : forall R, Frs HG (Frs HF R) [<=] R.
proof: Proof. intros R x H. do 2 destruct H. subst. do 2 destruct H. subst. rewrite Fr_epi. hyp. hyp. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)