proposition: Lemma Fl_epi : forall l, Fl HF (Fl HG l) = l.
proof: Proof. induction l; simpl; intros. refl. rewrite Fr_epi, IHl. refl. Qed.
imports: Coq(List Morphisms Setoid) CoLoR(LogicUtil ATrs VecUtil RelUtil SN ARules SetUtil NatUtil)