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; apply in_flat_map; auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)