proposition: Lemma elem_of_coGset_to_coPset X x : x ∈ coGset_to_coPset X ↔ x ∈ X.
proof: Proof. destruct X as [X|X]; simpl. - by rewrite elem_of_gset_to_coPset. - by rewrite elem_of_difference, elem_of_gset_to_coPset, (left_id True (∧)). Qed.
imports: stdpp(decidable finite gmap coPset) stdpp(options)