proposition: Lemma pred_finite_set (P : A → Prop) : pred_finite P ↔ (∃ X : C, ∀ x, P x → x ∈ X).
proof: Proof. split. - intros [xs Hfin]. exists (list_to_set xs). set_solver. - intros [X Hfin]. exists (elements X). set_solver. Qed.
imports: stdpp(relations) stdpp(options)