diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index f17fc27db86af45b1fd73975a49cea22034873cf..066d8873000d22b1f11bb4910608011f597757e0 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -249,6 +249,29 @@ Section fupd_derived.
   Proof. by rewrite {1}(fupd_intro_mask E E P) // fupd_trans. Qed.
   Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → ⊢@{PROP} |={E1,E2}=> |={E2,E1}=> emp.
   Proof. exact: fupd_intro_mask. Qed.
+
+  Lemma fupd_mask_subseteq E1 E2 P :
+    E2 ⊆ E1 →
+    ((|={E2,E1}=> emp) ={E2}=∗ P) ={E1,E2}=∗ P.
+  Proof.
+    intros HE.
+    (* Get an [emp] so we can apply [fupd_intro_mask']. *)
+    rewrite -[X in (X -∗ _)](left_id emp%I bi_sep).
+    rewrite {1}(fupd_intro_mask' E1 E2) //.
+    rewrite fupd_frame_r. by rewrite wand_elim_r fupd_trans.
+  Qed.
+  Lemma fupd_intro_mask_subseteq E1 E2 P :
+    E2 ⊆ E1 →
+    ((|={E2,E1}=> emp) -∗ P) ={E1,E2}=∗ P.
+  Proof.
+    intros. etrans; [|by apply fupd_mask_subseteq]. by rewrite -fupd_intro.
+  Qed.
+
+  Lemma fupd_mask_eq E1 E2 P : E1 = E2 → (|={E1}=> P) ={E1,E2}=∗ P.
+  Proof. intros <-. done. Qed.
+  Lemma fupd_intro_mask_eq E1 E2 P : E1 = E2 → P ={E1,E2}=∗ P.
+  Proof. intros <-. apply fupd_intro. 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.
   Lemma fupd_idemp E P : (|={E}=> |={E}=> P) ⊣⊢ |={E}=> P.
@@ -330,10 +353,6 @@ Section fupd_derived.
     rewrite {4}(union_difference_L _ _ HE). done.
   Qed.
 
-  Lemma fupd_mask_same E E1 P :
-    E = E1 → (|={E}=> P) -∗ (|={E,E1}=> P).
-  Proof. intros <-. done. Qed.
-
   Lemma fupd_sep E P Q : (|={E}=> P) ∗ (|={E}=> Q) ={E}=∗ P ∗ Q.
   Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.