diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index 33af48462675800787e244d8aa7005e1695ff580..553ee278eb22c24b7c47d26abcc164042dfbad1b 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -65,7 +65,7 @@ Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P} :
 Proof.
   iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
   iAssert (|={⊤,E2}=> P)%I as "H".
-  { iMod fupd_intro_mask'; last iApply Hfupd. done. }
+  { iMod Hfupd as "[_ $]". done. }
   rewrite uPred_fupd_eq /uPred_fupd_def.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index e987fc3f22f86184d5b9ef5122767598d47f3b32..3f9f00d6f0975f8c94dd0ab4b3d3283bc9be3c69 100644
--- a/iris/base_logic/lib/invariants.v
+++ b/iris/base_logic/lib/invariants.v
@@ -140,8 +140,8 @@ Section inv.
     rewrite inv_eq. iIntros (??) "#HinvP #HinvQ !>"; iIntros (E ?).
     iMod ("HinvP" with "[%]") as "[$ HcloseP]"; first set_solver.
     iMod ("HinvQ" with "[%]") as "[$ HcloseQ]"; first set_solver.
-    iMod (fupd_intro_mask' _ (E ∖ ↑N)) as "Hclose"; first set_solver.
-    iIntros "!> [HP HQ]".
+    iApply fupd_intro_adjust_mask; first set_solver.
+    iIntros "Hclose [HP HQ]".
     iMod "Hclose" as %_. iMod ("HcloseQ" with "HQ") as %_. by iApply "HcloseP".
   Qed.
 
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 731e88dc298023328c874d01d67f0ed975318f50..4f34564dae861c24e3a999efcf5a40d3e9f1d2d6 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -55,9 +55,9 @@ Section definition.
     Eo1 ⊆ Eo2 →
     atomic_acc Eo1 Ei α P β Φ -∗ atomic_acc Eo2 Ei α P β Φ.
   Proof.
-    iIntros (HE) "Hstep".
-    iMod fupd_intro_mask' as "Hclose1"; first done.
-    iMod "Hstep" as (x) "[Hα Hclose2]". iIntros "!>". iExists x.
+    iIntros (HE) "Hstep". rewrite /atomic_acc.
+    iMod "Hstep" as "[Hclose Hstep]".
+    iDestruct "Hstep" as (x) "[Hα Hclose2]". iIntros "!>". iExists x.
     iFrame. iSplitWith "Hclose2".
     - iIntros "Hα". iMod ("Hclose2" with "Hα") as "$". done.
     - iIntros (y) "Hβ". iMod ("Hclose2" with "Hβ") as "$". done.
@@ -311,7 +311,7 @@ Section lemmas.
     atomic_acc Eo Ei α P β Φ).
   Proof.
     iIntros (? x) "Hα Hclose".
-    iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first set_solver.
+    iApply fupd_intro_adjust_mask; first done. iIntros "Hclose'".
     iExists x. iFrame. iSplitWith "Hclose".
     - iIntros "Hα". iMod "Hclose'" as "_". iApply "Hclose". done.
     - iIntros (y) "Hβ". iMod "Hclose'" as "_". iApply "Hclose". done.
@@ -330,7 +330,7 @@ Section lemmas.
        to happen only if one argument is a constructor. *)
     iIntros (_) "Hinner >Hacc". iDestruct "Hacc" as (x') "[Hα' Hclose]".
     iMod ("Hinner" with "Hα'") as (x) "[Hα Hclose']".
-    iMod (fupd_intro_mask') as "Hclose''"; last iModIntro; first done.
+    iApply fupd_intro_adjust_mask; first done. iIntros "Hclose''".
     iExists x. iFrame. iSplitWith "Hclose'".
     - iIntros "Hα". iMod "Hclose''" as "_".
       iMod ("Hclose'" with "Hα") as "[Hβ' HPas]".
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 8ef588bb5f4ad3321d833504c94d1c6f788acb83..59c16cf867bb926e5c5f696ed0719943a07a1238 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -283,6 +283,17 @@ Section fupd_derived.
     (Q -∗ (|={E2,E3}=> P)) → (|={E1,E2}=> Q) -∗ (|={E1,E3}=> P).
   Proof. intros ->. rewrite fupd_trans //. Qed.
 
+  Lemma fupd_intro_adjust_mask E1 E2 P:
+    E2 ⊆ E1 →
+    ((|={E2,E1}=> emp) -∗ P) -∗ |={E1,E2}=> P.
+  Proof.
+    intros HE.
+    (* Get an [emp] so we can apply [fupd_intro_mask']. *)
+    rewrite -[X in (X -∗ _)](right_id emp%I).
+    rewrite {2}(fupd_intro_mask' E1 E2) //.
+    rewrite fupd_frame_l. apply fupd_mono. rewrite wand_elim_l. done.
+  Qed.
+
   Lemma fupd_mask_frame_r E1 E2 Ef P :
     E1 ## Ef → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P.
   Proof.
diff --git a/iris/program_logic/ectx_lifting.v b/iris/program_logic/ectx_lifting.v
index 016e13f4cf59abdc34dc72ffc774aa0f8c701682..c11dc8534a395d05cc4e4582f0536dc63c666b7f 100644
--- a/iris/program_logic/ectx_lifting.v
+++ b/iris/program_logic/ectx_lifting.v
@@ -62,8 +62,7 @@ Lemma wp_lift_pure_head_stuck E Φ e :
   ⊢ WP e @ E ?{{ Φ }}.
 Proof using Hinh.
   iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
-  iIntros (σ κs n) "_". iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
-  by auto.
+  iIntros (σ κs n) "_". iApply fupd_intro_adjust_mask; by auto with set_solver.
 Qed.
 
 Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
diff --git a/iris/program_logic/lifting.v b/iris/program_logic/lifting.v
index 04189b77f26368933be32dce59b8317189c9ec0e..d6ef2b9221b4b741bed33afa9415edea1134595b 100644
--- a/iris/program_logic/lifting.v
+++ b/iris/program_logic/lifting.v
@@ -61,7 +61,7 @@ Proof.
   iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
   { specialize (Hsafe inhabitant). destruct s; eauto using reducible_not_val. }
   iIntros (σ1 κ κs n) "Hσ". iMod "H".
-  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
+  iApply fupd_intro_adjust_mask; first set_solver. iIntros "Hclose". iSplit.
   { iPureIntro. destruct s; done. }
   iNext. iIntros (e2 σ2 efs ?).
   destruct (Hstep κ σ1 e2 σ2 efs) as (-> & <- & ->); auto.
@@ -76,7 +76,7 @@ Proof.
   iIntros (Hstuck) "_". iApply wp_lift_stuck.
   - destruct(to_val e) as [v|] eqn:He; last done.
     rewrite -He. by case: (Hstuck inhabitant).
-  - iIntros (σ κs n) "_". by iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
+  - iIntros (σ κs n) "_". iApply fupd_intro_adjust_mask; auto with set_solver.
 Qed.
 
 (* Atomic steps don't need any mask-changing business here, one can
@@ -94,8 +94,8 @@ Proof.
   iIntros (?) "H".
   iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1 κ κs n) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
-  iMod (fupd_intro_mask' E1 ∅) as "Hclose"; first set_solver.
-  iIntros "!>" (e2 σ2 efs ?). iMod "Hclose" as "_".
+  iApply fupd_intro_adjust_mask; first set_solver.
+  iIntros "Hclose" (e2 σ2 efs ?). iMod "Hclose" as "_".
   iMod ("H" $! e2 σ2 efs with "[#]") as "H"; [done|].
   iMod (fupd_intro_mask' E2 ∅) as "Hclose"; [set_solver|]. iIntros "!> !>".
   iMod "Hclose" as "_". iMod "H" as "($ & HQ & $)".
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index b39de3365c038b7d7c3599b5c055d879c39fd697..1dc6c1877ebbcc30e9699ceb628c6d9dc877803a 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -146,8 +146,8 @@ Section lifting.
     iIntros (Hsafe Hstep) "H"; iApply wp_lift_step.
     { specialize (Hsafe inhabitant). destruct s; last done.
       by eapply reducible_not_val. }
-    iIntros (σ1 κ κs n) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-    iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?).
+    iIntros (σ1 κ κs n) "Hσ". iApply fupd_intro_adjust_mask; first set_solver.
+    iIntros "Hclose". iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?).
     destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
     by iMod "Hclose"; iModIntro; iFrame; iApply "H".
   Qed.
@@ -162,8 +162,8 @@ Section lifting.
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros (?) "[Hσ H]"; iApply ownP_lift_step.
-    iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-    iModIntro; iExists σ1; iFrame; iSplit; first by destruct s.
+    iApply fupd_intro_adjust_mask; first set_solver.
+    iIntros "Hclose". iExists σ1; iFrame; iSplit; first by destruct s.
     iNext; iIntros (κ e2 σ2 efs ?) "Hσ".
     iDestruct ("H" $! κ e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
     destruct (to_val e2) eqn:?; last by iExFalso.
diff --git a/iris/program_logic/total_lifting.v b/iris/program_logic/total_lifting.v
index ba799dd8f494c258f104420e457c412a3f1739b8..b527c7bcceb9b415da1f3417e67db7f2c52ae09d 100644
--- a/iris/program_logic/total_lifting.v
+++ b/iris/program_logic/total_lifting.v
@@ -35,7 +35,7 @@ Proof.
   iIntros (Hsafe Hstep) ">H". iApply twp_lift_step.
   { eapply reducible_not_val, reducible_no_obs_reducible, (Hsafe inhabitant). }
   iIntros (σ1 κs n) "Hσ".
-  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
+  iApply fupd_intro_adjust_mask; first by set_solver. iIntros "Hclose". iSplit.
   { iPureIntro. destruct s; auto. }
   iIntros (κ e2 σ2 efs ?). destruct (Hstep σ1 κ e2 σ2 efs) as (->&<-&->); auto.
   iMod "Hclose" as "_". iModIntro.
@@ -58,8 +58,8 @@ Proof.
   iIntros (?) "H".
   iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1 κs n) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
-  iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-  iIntros "!>" (κ e2 σ2 efs) "%". iMod "Hclose" as "_".
+  iApply fupd_intro_adjust_mask; first set_solver.
+  iIntros "Hclose" (κ e2 σ2 efs) "%". iMod "Hclose" as "_".
   iMod ("H" $! κ e2 σ2 efs with "[#]") as "($ & $ & HΦ & $)"; first by eauto.
   destruct (to_val e2) eqn:?; last by iExFalso.
   iApply twp_value; last done. by apply of_to_val.
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 5dadf421fd2816d089a3115d8fdb20c86a7b7abe..984c7fc99bcb5c5484cbb38c67df0a2dfd86a85a 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -115,8 +115,8 @@ Proof.
   iIntros "!>" (e E1 Φ) "IH"; iIntros (E2 Ψ HE) "HΦ".
   rewrite !twp_unfold /twp_pre. destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
-  iIntros (σ1 κs n) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
-  iMod ("IH" with "[$]") as "[% IH]".
+  iIntros (σ1 κs n) "Hσ".
+  iMod ("IH" with "[$]") as "[Hclose [% IH]]".
   iModIntro; iSplit; [by destruct s1, s2|]. iIntros (κ e2 σ2 efs Hstep).
   iMod ("IH" with "[//]") as (?) "(Hσ & IH & IHefs)"; auto.
   iMod "Hclose" as "_"; iModIntro.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index c10cd66f564f7083d3a6276ffbcd5a7042dd39a1..804060eaccf89e8e60bed4f167874d0da7a7e6c3 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -101,8 +101,8 @@ Proof.
   rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:?.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
-  iIntros (σ1 κ κs n) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
-  iMod ("H" with "[$]") as "[% H]".
+  iIntros (σ1 κ κs n) "Hσ".
+  iMod ("H" with "[$]") as "[Hclose [% H]]".
   iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
   iMod ("H" with "[//]") as "H". iIntros "!> !>".
   iMod "H" as "(Hσ & H & Hefs)".
diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index 5fd7fea8bda20e776893c76b74852bc4a532b877..8fc10841c7318bcd2a79ebb8d7b44dfc7ccd2296 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -178,4 +178,16 @@ Proof.
   iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
   iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
 Qed.
+
+Global Instance elim_modal_fupd_fupd_adjust_mask `{!BiFUpd PROP} p E1 E1' E2 E2' P Q :
+  ElimModal (E1' ⊆ E1) p false
+    (|={E1',E2'}=> P) ((|={E1',E1}=> emp) ∗ P)
+    (|={E1,E2}=> Q) (|={E2',E2}=> Q) | 20.
+Proof.
+  rewrite /ElimModal /= intuitionistically_if_elim.
+  iIntros (HE) "[HP Hcont]".
+  iMod fupd_intro_mask' as "Hclose"; first exact HE.
+  iMod "HP" as "HP". iApply "Hcont". iSplitR "HP"; done.
+Qed.
+
 End class_instances_updates.