proposition: Lemma fmap_gset_to_gmap {A B} (f : A → B) (X : gset K) (x : A) : f <$> gset_to_gmap x X = gset_to_gmap (f x) X.
proof: Proof. apply map_eq; intros j. rewrite lookup_fmap, !lookup_gset_to_gmap. by simplify_option_eq. Qed.
imports: stdpp(mapset pmap) stdpp(options)