proposition: Theorem in_flat_map: forall (l : list B) (f : B -> list C) a b, In a (f b) -> In b l -> In a (flat_map f l).
proof: Proof. intros l g; elim l; simpl; auto. intros a l0 H a0 b H0 [H1|H1]; apply in_or_app; auto. left; rewrite H1; auto. right; apply H with ( b := b ); auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat