diff --git a/stdpp/mapset.v b/stdpp/mapset.v
index 46f0c745e1d1f66d7d5c8e0f9b747f1811a48ddc..689f556dd11be6047720637738cbf8c385fe634b 100644
--- a/stdpp/mapset.v
+++ b/stdpp/mapset.v
@@ -128,11 +128,14 @@ Proof.
   - destruct (Is_true_reflect (f a)); naive_solver.
   - naive_solver.
 Qed.
-Local Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
+
+Local Instance mapset_dom {A} : Dom (M A) (mapset M) := λ m,
+  Mapset $ fmap (λ _, ()) m.
 Local Instance mapset_dom_spec: FinMapDom K M (mapset M).
 Proof.
-  split; try apply _. intros. unfold dom, mapset_dom, is_Some.
-  rewrite elem_of_mapset_dom_with; naive_solver.
+  split; try apply _. intros A m i.
+  unfold dom, mapset_dom, is_Some, elem_of, mapset_elem_of; simpl.
+  rewrite lookup_fmap. destruct (m !! i); naive_solver.
 Qed.
 End mapset.