proposition: Lemma coGpick_elem_of `{Countable A, Infinite A} (X : coGset A) : ¬set_finite X → coGpick X ∈ X.
proof: Proof. unfold coGpick. destruct X as [X|X]; rewrite coGset_finite_spec; simpl; [done|]. by intros _; apply is_fresh. Qed.
imports: stdpp(decidable finite gmap coPset) stdpp(options)