proposition: Lemma in_map_in : forall (A B : Set) (f : A -> B) b l, In b (map f l) -> exists a, In a l /\ f a = b.
proof: Proof. intros A B f b l; induction l as [ | a l ]. contradiction. intro In_b; elim In_b; clear In_b; intro In_b. exists a; split; trivial; left; trivial. elim (IHl In_b); intros a' [H1 H2]; exists a'; split; trivial; right; trivial. Qed.
imports: List Arith