proposition: Lemma In_mapI : forall A B (f: A -> B) x l (IN: In x l), In (f x) (map f l).
proof: Proof. induction l; simpl; intros; auto. case IN; intros. - rewrite H. left; auto. - right. apply IHl; auto. Qed.
imports: Coq(List Permutation)