diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 07c9185c845e5b52f4666d96e1267bdeb849191e..ab81170370030e432c7c4d651775edfc5f00cae9 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -133,7 +133,7 @@ Section fupd_derived.
 
   Lemma fupd_intro E P : P ={E}=∗ P.
   Proof. rewrite -bupd_fupd. apply bupd_intro. Qed.
-  Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → (|={E1,E2}=> |={E2,E1}=> emp : PROP)%I.
+  Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → (|={E1,E2}=> |={E2,E1}=> bi_emp (PROP:=PROP))%I.
   Proof. exact: fupd_intro_mask. Qed.
   Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P.
   Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.