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; elim l; simpl; auto. intros tmp; case tmp. intros a0 l0 H [H1|H1]; auto. exists a0; auto. case (H H1); intros a1 [H2 H3]; exists a1; auto. Qed.
imports: List Arith Tactic Inverse_Image Wf_nat