proposition: Lemma map_flat_map : forall A B C , forall f : B -> list C, forall g : C -> A, forall l : list B, map g (flat_map f l) = flat_map (compose (map g) f) l.
proof: Proof. induction l; simpl; sp. rw map_app. rewrite IHl. unfold compose; auto. Qed.
imports: UsefulTypes bin_rels Omega