proposition: Lemma Permutation_undup A (l l' : list A) : Permutation l l' -> Permutation (undup l) (undup l').
proof: Proof. ins; eapply NoDup_Permutation; ins; rewrite !in_undup_iff. split; eauto using Permutation_in, Permutation_sym. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation