proposition: Lemma coGset_finite_spec X : set_finite X ↔ coGset_finite X.
proof: Proof. destruct X as [X|X]; unfold set_finite, elem_of at 1, coGset_elem_of; simpl. - split; [done|intros _]. exists (elements X). set_solver. - split; [intros [Y HXY]%(pred_finite_set(C:=gset A))|done]. by destruct (exist_fresh (X ∪ Y)) as [? [?%HXY ?]%not_elem_of_union]. Qed.
imports: stdpp(decidable finite gmap coPset) stdpp(options)