proposition: Lemma In_flat_map_elim : forall l y, In y (flat_map f l) -> exists x, In x l /\ In y (f x).
proof: Proof. intros. exact (proj1 (@in_flat_map _ _ _ _ _) H). Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)