proposition: Lemma 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. MProof. intros A B f l x. elim l &> [i: ~~ | \x' l' IHl']. - simpl. pintros [|]. - simpl. pintros [| \H | \H]. + rewrite H. left. T.reflexivity. + right. apply IHl'. apply H. Qed.