diff --git a/iris/algebra/dyn_reservation_map.v b/iris/algebra/dyn_reservation_map.v
index 6570c88653aa2a674a1af4b08ff7f101448dba19..f11f6b6b3d9e65bbc249a78536b2a8bf2d4f8e10 100644
--- a/iris/algebra/dyn_reservation_map.v
+++ b/iris/algebra/dyn_reservation_map.v
@@ -282,10 +282,10 @@ Section cmra.
     intros [Hmap [Hinf Hdisj]].
     (* Pick a fresh set disjoint from the existing tokens [Ef] and map [mf],
        such that both that set [E1] and the remainder [E2] are infinite. *)
-    edestruct (coPset_split_infinite (⊤ ∖ (Ef ∪ dom coPset mf))) as
+    edestruct (coPset_split_infinite (⊤ ∖ (Ef ∪ (gset_to_coPset $ dom (gset _) mf)))) as
         (E1 & E2 & HEunion & HEdisj & HE1inf & HE2inf).
     { rewrite -difference_difference_L.
-        by apply difference_infinite, dom_finite. }
+      by apply difference_infinite, gset_to_coPset_finite. }
     exists (dyn_reservation_map_token E1).
     split; first by apply HQ. clear HQ.
     rewrite dyn_reservation_map_validN_eq /=.