diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index ba7a2e4f27e149a3b4313f85168192e3ace2292f..b44fb1ef80e7b75f80c0f5d6b91ec3d36aab5aca 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -93,7 +93,7 @@ Section upred.
     Proof. by uPred.unseal. Qed.
 
     Lemma reservation_map_data_validI k b :
-      ✓ reservation_map_data k b ⊣⊢@{uPredI M} ✓ b.
+      ✓ reservation_map_data k b ⊣⊢ ✓ b.
     Proof.
       rewrite reservation_validI /= singleton_validI.
       apply (anti_symm _); first by rewrite bi.and_elim_l.