diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index f36e712e15b35edf52a60c4a45e47f3181fb98d0..480faeda6efea6af5b9cc3cc24a70fd8422d6e36 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -203,6 +203,13 @@ Section fupd_derived.
   Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ∗ (P -∗ Q) ={E1,E2}=∗ Q.
   Proof. by rewrite fupd_frame_r wand_elim_r. Qed.
 
+  Lemma fupd_mask_weaken E1 E2 P `{!Absorbing P} : E2 ⊆ E1 → P ={E1,E2}=∗ P.
+  Proof.
+    intros ?. rewrite -{1}(right_id emp%I bi_sep P%I).
+    rewrite (fupd_intro_mask E1 E2 emp%I) //.
+    by rewrite fupd_frame_l sep_elim_l.
+  Qed.
+
   Lemma fupd_trans_frame E1 E2 E3 P Q :
     ((Q ={E2,E3}=∗ emp) ∗ |={E1,E2}=> (Q ∗ P)) ={E1,E3}=∗ P.
   Proof.