proposition: Lemma pred_infinite_set (P : A → Prop) : pred_infinite P ↔ (∀ X : C, ∃ x, P x ∧ x ∉ X).
proof: Proof. split. - intros Hinf X. destruct (Hinf (elements X)). set_solver. - intros Hinf xs. destruct (Hinf (list_to_set xs)). set_solver. Qed.
imports: stdpp(relations) stdpp(options)