proposition: Lemma map_NoDup' : forall (A B : Set) (ls : list A) (f : A -> B), NoDup ls -> (forall a1 a2 : A, In a1 ls -> In a2 ls ->a1 <> a2 -> f a1 <> f a2) -> NoDup (map f ls).
proof: Proof. induction ls; intuition; simpl in *; econstructor. inversion H; clear H; subst. intuition. eapply in_map_iff in H. destruct H. intuition. eapply H0. right. eauto. left. eauto. intuition. subst. intuition. intuition. inversion H; clear H; subst. eapply IHls; intuition. eapply H0. right. eapply H. right. eapply H1. intuition. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation