proposition: Lemma gset_to_gmap_set_to_map {A} (X : gset K) (x : A) : gset_to_gmap x X = set_to_map (.,x) X.
proof: Proof. apply map_eq; intros k. apply option_eq; intros y. rewrite lookup_gset_to_gmap_Some, lookup_set_to_map; naive_solver. Qed.
imports: stdpp(mapset pmap) stdpp(options)