proposition: Theorem In_map : forall (A B : Type) (f : A -> B) (l : list A) (x : A), In x l -> In (f x) (map f l).
proof: Proof. intros A B f l x. induction l as [|x' l' IHl']. - simpl. intros []. - simpl. intros [H | H]. + rewrite H. left. reflexivity. + right. apply IHl'. apply H. Qed.