proposition: Lemma in_undup_iff A (x : A) (l : list A) : In x (undup l) <-> In x l.
proof: Proof. induction l; split; ins; desf; ins; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation