proposition: Lemma gset_to_gmap_dom {A B} (m : gmap K A) (y : B) : gset_to_gmap y (dom m) = const y <$> m.
proof: Proof. apply map_eq; intros j. rewrite lookup_fmap, lookup_gset_to_gmap. destruct (m !! j) as [x|] eqn:?. - by rewrite option_guard_True by (rewrite elem_of_dom; eauto). - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto). Qed.
imports: stdpp(mapset pmap) stdpp(options)