proposition: Lemma undup_nonnil A (l : list A) : l <> nil -> undup l <> nil.
proof: Proof. induction l; ins; desf. by eapply in_undup_iff in i; intro X; rewrite X in *. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation