proposition: Lemma set_finiteE A (s : A -> Prop) : set_finite s <-> exists findom, NoDup findom /\ s ≡₁ (fun x => In x findom).
proof: Proof. repeat autounfold with unfolderDb; intuition; desf; eauto. exists (undup (filterP s findom)); splits; ins. all: rewrite in_undup_iff, in_filterP_iff in *; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation