fact: Fixpoint undup A (l: list A) := match l with nil => nil | x :: l => ifP (In x l) then undup l else x :: undup l end.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation