proposition: Lemma elem_of_gset_to_coPset X i : i ∈ gset_to_coPset X ↔ i ∈ X.
proof: Proof. destruct X as [m]. unfold elem_of, coPset_elem_of; simpl. by rewrite elem_of_Pset_to_coPset_raw, lookup_gmap_to_pmap. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)