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 1; ins; vauto. constructor; eauto. intro; rewrite in_map_iff in *; desf. edestruct H1; try eapply H2; eauto. intro; desf. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation