diff --git a/iris/algebra/dyn_reservation_map.v b/iris/algebra/dyn_reservation_map.v
index f11f6b6b3d9e65bbc249a78536b2a8bf2d4f8e10..51d5affda6ea54498c060ee4571462efe526e419 100644
--- a/iris/algebra/dyn_reservation_map.v
+++ b/iris/algebra/dyn_reservation_map.v
@@ -294,7 +294,7 @@ Section cmra.
     - eapply set_infinite_subseteq, HE2inf. set_solver.
     - intros i. rewrite left_id_L. destruct (Hdisj i) as [?|Hi]; first by left.
       destruct (mf !! i) as [p|] eqn:Hp; last by left.
-      apply (elem_of_dom_2 (D:=coPset)) in Hp. right. set_solver.
+      apply (elem_of_dom_2 (D:=gset _)), elem_of_gset_to_coPset in Hp. right. set_solver.
   Qed.
   Lemma dyn_reservation_map_reserve' :
     ε ~~>: (λ x, ∃ E, set_infinite E ∧ x = dyn_reservation_map_token E).