proposition: Lemma lookup_gset_to_gmap {A} (x : A) (X : gset K) i : gset_to_gmap x X !! i = (guard (i ∈ X);; Some x).
proof: Proof. destruct X as [X]. unfold gset_to_gmap, gset_elem_of, elem_of, mapset_elem_of; simpl. rewrite lookup_fmap. case_guard; destruct (X !! i) as [[]|]; naive_solver. Qed.
imports: stdpp(mapset pmap) stdpp(options)