diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index 33af48462675800787e244d8aa7005e1695ff580..44ddb2875c8daaeda2c3c5c8f2801e71b53aa64a 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. }
+  { iApply (fupd_mask_weaken E1); first done. iIntros "_". iApply Hfupd. }
   rewrite uPred_fupd_eq /uPred_fupd_def.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
@@ -94,5 +94,5 @@ Lemma step_fupdN_soundness' `{!invPreG Σ} φ n :
 Proof.
   iIntros (Hiter). eapply (step_fupdN_soundness _ n).
   iIntros (Hinv). iPoseProof (Hiter Hinv) as "Hiter".
-  iApply (step_fupdN_wand with "Hiter"). by iApply fupd_mask_weaken.
+  iApply (step_fupdN_wand with "Hiter"). by iApply fupd_mask_intro_discard.
 Qed.
diff --git a/iris/base_logic/lib/invariants.v b/iris/base_logic/lib/invariants.v
index e987fc3f22f86184d5b9ef5122767598d47f3b32..91f87d5deda33c5e767ac397fd70e00696d6fe3b 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_mask_intro; 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..266e3ec89a12764b134659aa347791fd3d25681c 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -56,7 +56,7 @@ Section definition.
     atomic_acc Eo1 Ei α P β Φ -∗ atomic_acc Eo2 Ei α P β Φ.
   Proof.
     iIntros (HE) "Hstep".
-    iMod fupd_intro_mask' as "Hclose1"; first done.
+    iApply (fupd_mask_weaken Eo1); first done. iIntros "Hclose1".
     iMod "Hstep" as (x) "[Hα Hclose2]". iIntros "!>". iExists x.
     iFrame. iSplitWith "Hclose2".
     - iIntros "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_mask_intro; first set_solver. 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_mask_intro; first set_solver. iIntros "Hclose''".
     iExists x. iFrame. iSplitWith "Hclose'".
     - iIntros "Hα". iMod "Hclose''" as "_".
       iMod ("Hclose'" with "Hα") as "[Hβ' HPas]".
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index f09bf301bf72cc17aec70439030e9b23519a2eb8..74b2e3fb75d793e64f6bebdae6b4c2bbf840e288 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -894,7 +894,7 @@ Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
 Proof.
   split; rewrite monPred_fupd_eq.
   - split=>/= i. solve_proper.
-  - intros E1 E2 P HE12. split=>/= i. by apply fupd_intro_mask.
+  - intros E1 E2 P HE12. split=>/= i. by apply fupd_mask_intro_subseteq.
   - intros E1 E2 P. split=>/= i. by rewrite monPred_at_except_0 except_0_fupd.
   - intros E1 E2 P Q HPQ. split=>/= i. by rewrite HPQ.
   - intros E1 E2 E3 P. split=>/= i. apply fupd_trans.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 8ef588bb5f4ad3321d833504c94d1c6f788acb83..5a1c7051621b411eecbb6078fcc4277e579a0d3d 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -68,14 +68,20 @@ Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
 }.
 
 Record BiFUpdMixin (PROP : bi) `(FUpd PROP) := {
-  bi_fupd_mixin_fupd_ne E1 E2 : NonExpansive (fupd (PROP:=PROP) E1 E2);
-  bi_fupd_mixin_fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P;
-  bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P;
-  bi_fupd_mixin_fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q;
-  bi_fupd_mixin_fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P;
+  bi_fupd_mixin_fupd_ne E1 E2 :
+    NonExpansive (fupd (PROP:=PROP) E1 E2);
+  bi_fupd_mixin_fupd_mask_intro_subseteq E1 E2 (P : PROP) :
+    E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P;
+  bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) :
+    ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P;
+  bi_fupd_mixin_fupd_mono E1 E2 (P Q : PROP) :
+    (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q;
+  bi_fupd_mixin_fupd_trans E1 E2 E3 (P : PROP) :
+    (|={E1,E2}=> |={E2,E3}=> P) ⊢ |={E1,E3}=> P;
   bi_fupd_mixin_fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
     E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ={E1 ∪ Ef,E2 ∪ Ef}=∗ P;
-  bi_fupd_mixin_fupd_frame_r E1 E2 (P R : PROP) : (|={E1,E2}=> P) ∗ R ={E1,E2}=∗ P ∗ R;
+  bi_fupd_mixin_fupd_frame_r E1 E2 (P R : PROP) :
+    (|={E1,E2}=> P) ∗ R ={E1,E2}=∗ P ∗ R;
 }.
 
 Class BiBUpd (PROP : bi) := {
@@ -147,8 +153,8 @@ Section fupd_laws.
 
   Global Instance fupd_ne E1 E2 : NonExpansive (@fupd PROP _ E1 E2).
   Proof. eapply bi_fupd_mixin_fupd_ne, bi_fupd_mixin. Qed.
-  Lemma fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
-  Proof. eapply bi_fupd_mixin_fupd_intro_mask, bi_fupd_mixin. Qed.
+  Lemma fupd_mask_intro_subseteq E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
+  Proof. eapply bi_fupd_mixin_fupd_mask_intro_subseteq, bi_fupd_mixin. Qed.
   Lemma except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P.
   Proof. eapply bi_fupd_mixin_except_0_fupd, bi_fupd_mixin. Qed.
   Lemma fupd_mono E1 E2 (P Q : PROP) : (P ⊢ Q) → (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
@@ -246,9 +252,9 @@ Section fupd_derived.
   Proof. intros P Q; apply fupd_mono. Qed.
 
   Lemma fupd_intro E P : P ={E}=∗ P.
-  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.
+  Proof. by rewrite {1}(fupd_mask_intro_subseteq E E P) // fupd_trans. Qed.
+  Lemma fupd_mask_intro_subseteq_emp E1 E2 : E2 ⊆ E1 → ⊢@{PROP} |={E1,E2}=> |={E2,E1}=> emp.
+  Proof. exact: fupd_mask_intro_subseteq. 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.
@@ -258,6 +264,34 @@ Section fupd_derived.
     - apply fupd_intro.
   Qed.
 
+  (** Weaken the first mask of the goal from [E1] to [E2].
+      This lemma is intended to be [iApply]ed. *)
+  Lemma fupd_mask_weaken {E1} E2 {E3 P} :
+    E2 ⊆ E1 →
+    ((|={E2,E1}=> emp) ={E2,E3}=∗ P) -∗ |={E1,E3}=> 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_mask_intro_subseteq_emp E1 E2) //.
+    rewrite fupd_frame_r. by rewrite wand_elim_r fupd_trans.
+  Qed.
+
+  (** Introduction lemma for a mask-changing fupd.
+      This lemma is intended to be [iApply]ed. *)
+  Lemma fupd_mask_intro E1 E2 P :
+    E2 ⊆ E1 →
+    ((|={E2,E1}=> emp) -∗ P) -∗ |={E1,E2}=> P.
+  Proof.
+    intros. etrans; [|by apply fupd_mask_weaken]. by rewrite -fupd_intro.
+  Qed.
+
+  Lemma fupd_mask_intro_discard E1 E2 P `{!Absorbing P} : E2 ⊆ E1 → P ={E1,E2}=∗ P.
+  Proof.
+    intros. etrans; [|by apply fupd_mask_intro].
+    apply wand_intro_r. rewrite sep_elim_l. done.
+  Qed.
+
   Lemma fupd_frame_l E1 E2 R Q : (R ∗ |={E1,E2}=> Q) ={E1,E2}=∗ R ∗ Q.
   Proof. rewrite !(comm _ R); apply fupd_frame_r. Qed.
   Lemma fupd_wand_l E1 E2 P Q : (P -∗ Q) ∗ (|={E1,E2}=> P) ={E1,E2}=∗ Q.
@@ -265,13 +299,6 @@ 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.
@@ -318,7 +345,7 @@ Section fupd_derived.
     rewrite -(fupd_mask_frame E E'); first apply fupd_mono; last done.
     (* The most horrible way to apply fupd_intro_mask *)
     rewrite -[X in (X -∗ _)](right_id emp%I).
-    rewrite (fupd_intro_mask (E1 ∖ E2 ∪ E ∖ E1) (E ∖ E2) emp%I); last first.
+    rewrite (fupd_mask_intro_subseteq (E1 ∖ E2 ∪ E ∖ E1) (E ∖ E2) emp%I); last first.
     { rewrite {1}(union_difference_L _ _ HE). set_solver. }
     rewrite fupd_frame_l fupd_frame_r. apply fupd_elim.
     apply fupd_mono.
@@ -330,10 +357,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.
 
@@ -379,10 +402,10 @@ Section fupd_derived.
     Ei2 ⊆ Ei1 → Eo1 ⊆ Eo2 → (|={Eo1}[Ei1]▷=> P) ⊢ |={Eo2}[Ei2]▷=> P.
   Proof.
     intros ??. rewrite -(emp_sep (|={Eo1}[Ei1]â–·=> P)%I).
-    rewrite (fupd_intro_mask Eo2 Eo1 emp%I) //.
+    rewrite (fupd_mask_intro_subseteq Eo2 Eo1 emp%I) //.
     rewrite fupd_frame_r -(fupd_trans Eo2 Eo1 Ei2). f_equiv.
     rewrite fupd_frame_l -(fupd_trans Eo1 Ei1 Ei2). f_equiv.
-    rewrite (fupd_intro_mask Ei1 Ei2 (|={_,_}=> emp)%I) //.
+    rewrite (fupd_mask_intro_subseteq Ei1 Ei2 (|={_,_}=> emp)%I) //.
     rewrite fupd_frame_r. f_equiv.
     rewrite [X in (X ∗ _)%I]later_intro -later_sep. f_equiv.
     rewrite fupd_frame_r -(fupd_trans Ei2 Ei1 Eo2). f_equiv.
@@ -424,7 +447,7 @@ Section fupd_derived.
     by apply sep_mono; first apply later_intro.
   Qed.
 
-  Lemma step_fupdN_S_fupd n E P:
+  Lemma step_fupdN_S_fupd n E P :
     (|={E}[∅]▷=>^(S n) P) ⊣⊢ (|={E}[∅]▷=>^(S n) |={E}=> P).
   Proof.
     apply (anti_symm (⊢)); rewrite !Nat_iter_S_r; apply step_fupdN_mono;
@@ -444,7 +467,7 @@ Section fupd_derived.
     Lemma fupd_plainly_mask E E' P : (|={E,E'}=> ■ P) ⊢ |={E}=> P.
     Proof.
       rewrite -(fupd_plainly_mask_empty).
-      apply fupd_elim, (fupd_mask_weaken _ _ _). set_solver.
+      apply fupd_elim, (fupd_mask_intro_discard _ _ _). set_solver.
     Qed.
 
     Lemma fupd_plainly_elim E P : ■ P ={E}=∗ P.
@@ -491,7 +514,7 @@ Section fupd_derived.
       trans (∀ x, |={E1}=> Φ x)%I.
       { apply forall_mono=> x. by rewrite fupd_plain_mask. }
       rewrite fupd_plain_forall_2. apply fupd_elim.
-      rewrite {1}(plain (∀ x, Φ x)) (fupd_mask_weaken E1 E2 (■ _)%I) //.
+      rewrite {1}(plain (∀ x, Φ x)) (fupd_mask_intro_discard E1 E2 (■ _)%I) //.
       apply fupd_elim. by rewrite fupd_plainly_elim.
     Qed.
     Lemma fupd_plain_forall' E {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 901318923047d2072dca5bd25ce481b9a488cd5a..2749873336b643a647a7c77da81f60119e527c93 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -209,7 +209,7 @@ Proof.
   iMod Hwp as (stateI fork_post) "[Hσ Hwp]".
   iExists s, (λ σ κs _, stateI σ κs), [(λ v, ⌜φ v⌝%I)], fork_post => /=.
   iIntros "{$Hσ $Hwp} !>" (e2 t2' -> ? ?) "_ H _".
-  iApply fupd_mask_weaken; [done|]. iSplit; [|done].
+  iApply fupd_mask_intro_discard; [done|]. iSplit; [|done].
   iDestruct (big_sepL2_cons_inv_r with "H") as (e' ? ->) "[Hwp H]".
   iDestruct (big_sepL2_nil_inv_r with "H") as %->.
   iIntros (v2 t2'' [= -> <-]). by rewrite to_of_val.
@@ -234,5 +234,5 @@ Proof.
   iDestruct (big_sepL2_cons_inv_r with "H") as (? ? ->) "[_ H]".
   iDestruct (big_sepL2_nil_inv_r with "H") as %->.
   iDestruct ("Hφ" with "Hσ") as (E) ">Hφ".
-  by iApply fupd_mask_weaken; first set_solver.
+  by iApply fupd_mask_intro_discard; first set_solver.
 Qed.
diff --git a/iris/program_logic/ectx_lifting.v b/iris/program_logic/ectx_lifting.v
index 016e13f4cf59abdc34dc72ffc774aa0f8c701682..189a1a216f8f216c771d69e023e41a779d1ee8c1 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_mask_intro; 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..ac6e173053892bc6321cb9b5af74a08115e3541b 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_mask_intro; 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_mask_intro; auto with set_solver.
 Qed.
 
 (* Atomic steps don't need any mask-changing business here, one can
@@ -94,10 +94,10 @@ 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_mask_intro; 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 "!> !>".
+  iApply fupd_mask_intro; first set_solver. iIntros "Hclose !>".
   iMod "Hclose" as "_". iMod "H" as "($ & HQ & $)".
   destruct (to_val e2) eqn:?; last by iExFalso.
   iApply wp_value; last done. by apply of_to_val.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index b39de3365c038b7d7c3599b5c055d879c39fd697..bbd50bc3ba84d2df311b69051aed17e9e6f97f6d 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_mask_intro; 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_mask_intro; 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..c24d7127e12a2c75fdafd799cc467c50ae7c6236 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_mask_intro; 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_mask_intro; 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..e7e7f9bc39196cc9e67bed745d280512508753b1 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -115,7 +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.
+  iIntros (σ1 κs n) "Hσ".
+  iApply (fupd_mask_weaken E1); first done. iIntros "Hclose".
   iMod ("IH" with "[$]") as "[% IH]".
   iModIntro; iSplit; [by destruct s1, s2|]. iIntros (κ e2 σ2 efs Hstep).
   iMod ("IH" with "[//]") as (?) "(Hσ & IH & IHefs)"; auto.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index c10cd66f564f7083d3a6276ffbcd5a7042dd39a1..63e77fdf134fba1acc7c38000db2bed21b9a818f 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -101,7 +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.
+  iIntros (σ1 κ κs n) "Hσ".
+  iApply (fupd_mask_weaken E1); first done. iIntros "Hclose".
   iMod ("H" with "[$]") as "[% H]".
   iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
   iMod ("H" with "[//]") as "H". iIntros "!> !>".
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 3e8d41a8042d2ed291ce15625bc45f1ee674eab1..1e12166da52645f197a28b8b16a15fba9aa171ce 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -103,12 +103,12 @@ Section tests.
 
   Context (FU : BiFUpd PROP).
 
-  Lemma test_apply_fupd_intro_mask E1 E2 P :
+  Lemma test_apply_fupd_intro_mask_subseteq E1 E2 P :
     E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
-  Proof. iIntros. by iApply @fupd_intro_mask. Qed.
-  Lemma test_apply_fupd_intro_mask_2 E1 E2 P :
+  Proof. iIntros. by iApply @fupd_mask_intro_subseteq. Qed.
+  Lemma test_apply_fupd_intro_mask_subseteq_emp E1 E2 P :
     E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.
-  Proof. iIntros. iFrame. by iApply @fupd_intro_mask'. Qed.
+  Proof. iIntros. iFrame. by iApply @fupd_mask_intro_subseteq_emp. Qed.
 
   Lemma test_iFrame_embed_persistent (P : PROP) (Q: monPred) :
     Q ∗ □ ⎡P⎤ ⊢ Q ∗ ⎡P ∗ P⎤.