proposition: Theorem in_flat_map_ex: forall (l : list B) (f : B -> list C) a, In a (flat_map f l) -> (exists b , In b l /\ In a (f b) ).
proof: Proof. intros l g; elim l; simpl; auto. intros a H; case H. intros a l0 H a0 H0; case in_app_or with ( 1 := H0 ); simpl; auto. intros H1; exists a; auto. intros H1; case H with ( 1 := H1 ). intros b [H2 H3]; exists b; simpl; auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat