proposition: Theorem NoDup_map : forall (A B : Type)(f : A -> B)(ls : list A), NoDup (map f ls) -> (NoDup ls /\ (forall b1 b2, In b1 ls -> In b2 ls -> f b1 = f b2 -> b1 = b2)).
proof: Proof. induction ls; intros; simpl in *. intuition. econstructor. inversion H; clear H; subst. intuition. econstructor. intuition. eapply H2. eapply in_map_iff. econstructor. intuition. trivial. subst. trivial. subst. exfalso. eapply H2. eapply in_map_iff. econstructor. split. symmetry. eapply H5. trivial. subst. exfalso. eapply H2. eapply in_map_iff. econstructor. split. eapply H5. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation