proposition: Lemma subsetSingleFlatMap : forall {A B: Type} (f : B -> list A) (l: list B) (x:B), LIn x l -> subset (f x) (flat_map f l).
proof: Proof. introv Hin. introv Hp. apply lin_flat_map. eexists; eauto. Qed.
imports: UsefulTypes bin_rels Omega