proposition: Theorem in_map_inv: forall (b : B) (l : list A), In b (map f l) -> (exists a : A , In a l /\ b = f a ).
proof: Proof. intros b l H. rewrite in_map_iff in H. destruct H as [x [H1 H2]]. eauto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat