proposition: Theorem in_map_inv : forall (A B : Set) (f : A -> B) (l : list A) (x : A), (forall a b : A, f a = f b -> a = b) -> In (f x) (map f l) -> In x l.
proof: Proof. intros A B f l; elim l; simpl in |- *; auto. intros a l0 H' x H'0 H'1; elim H'1; clear H'1; intros H'2; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz