proposition: Lemma dom_gset_to_gmap {A} (X : gset K) (x : A) : dom (gset_to_gmap x X) = X.
proof: Proof. induction X as [| y X not_in IH] using set_ind_L. - rewrite gset_to_gmap_empty, dom_empty_L; done. - rewrite gset_to_gmap_union_singleton, dom_insert_L, IH; done. Qed.
imports: stdpp(mapset pmap) stdpp(options)