proposition: Lemma subsetFlatMap2Eauto: forall {A B : Type} (h : A) (f: A-> list B), subset (flat_map f [h,h]) (f h).
proof: Proof. introv Hin. allsimpl. repeat (rw in_app_iff in Hin). repeat (in_reasoning);cpx. Qed.
imports: UsefulTypes bin_rels Omega