proposition: Lemma In_map : forall (A B : Type) (xs : list A) (x : A) (f : A -> B), In x xs -> In (f x) (map f xs).
proof: Proof. induction xs; intros ? ? H; simpl in *. auto. destruct H; subst; auto. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Metalib.CoqUniquenessTac