proposition: Theorem in_flat_map_in : 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; apply in_flat_map; exists b; split; auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)