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