proposition: Lemma subset_flat_map : forall A B, forall f : A -> list B, forall l k, subset (flat_map f l) k <=> forall x, LIn x l -> subset (f x) k.
proof: Proof. induction l; simpl; sp. trw nil_subset_iff; split; sp. trw app_subset; split; sp; subst; sp; alltrewrite IHl; sp. Qed.
imports: UsefulTypes bin_rels Omega