proposition: Lemma nodup_undup A (l : list A) : NoDup (undup l).
proof: Proof. induction l; ins; desf; constructor; rewrite ?in_undup_iff in *; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation