proposition: Lemma lookup_gset_to_gmap_Some {A} (x : A) (X : gset K) i y : gset_to_gmap x X !! i = Some y ↔ i ∈ X ∧ x = y.
proof: Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
imports: stdpp(mapset pmap) stdpp(options)