proposition: Lemma In_map : forall A B (f: A->B) y l, In y (map f l) <-> exists x, f x = y /\ In x l.
proof: Proof. split; intros. - apply In_mapD; auto. - destruct H; destruct H. rewrite <- H. eapply In_mapI in H0; eauto. Qed.
imports: Coq(List Permutation)