proposition: Lemma nodup_map: forall (A B: Type) (f: A -> B) (l: list A), NoDup l -> (forall x y, In x l -> In y l -> x <> y -> f x <> f y) -> NoDup (map f l).
proof: Proof. induction l; simpl; intros; [constructor|]. inversion H; subst. constructor; eauto. intro; rewrite In_map in *. destruct H1; destruct H1. edestruct H0; try eapply H1; eauto. intro. contradict H3. rewrite <- H5. auto. Qed.
imports: Coq(List Permutation)