proposition: Lemma map_NoDup : forall (A B : Set)(ls : list A)(f : A -> B), NoDup ls -> (forall a1 a2, a1 <> a2 -> (f a1) <> (f a2)) -> NoDup ((map f) ls).
proof: Proof. induction ls; intuition; simpl in *. econstructor. inversion H; subst; clear H. econstructor. intuition. apply in_map_iff in H. destruct H. intuition. eapply H0; eauto. intuition. subst. intuition. eapply IHls; eauto. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith