proposition: Lemma elem_of_coPset_to_gset X i : set_finite X → i ∈ coPset_to_gset X ↔ i ∈ X.
proof: Proof. intros ?. rewrite <-elem_of_coPset_to_Pset by done. destruct X as [X ?]. unfold elem_of, gset_elem_of, mapset_elem_of, coPset_to_gset; simpl. by rewrite lookup_pmap_to_gmap. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)