proposition: Lemma nodup_mapD A B (f : A-> B) l : NoDup (map f l) -> NoDup l.
proof: Proof. induction l; ins; rewrite !nodup_cons, in_map_iff in *; desf; eauto 8. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation