proposition: Lemma lookup_gset_to_gmap_None {A} (x : A) (X : gset K) i : gset_to_gmap x X !! i = None ↔ i ∉ X.
proof: Proof. rewrite lookup_gset_to_gmap. simplify_option_eq; naive_solver. Qed.
imports: stdpp(mapset pmap) stdpp(options)