proposition: Lemma Injective_map_NoDup A B (f:A->B) (l:list A) : Injective f -> NoDup l -> NoDup (map f l).
proof: Proof. intros Ij. induction 1 as [|x l X N IH]; simpl; constructor; trivial. rewrite in_map_iff. intros (y & E & Y). apply Ij in E. now subst. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec