proposition: Lemma In_flat_map_intro : forall x l y, In y l -> In x (f y) -> In x (flat_map f l).
proof: Proof. intros. apply (proj2 (@in_flat_map _ _ f l x)). exists y. auto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)