diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index b04511cec7d03b90b569511cd8eb80feba794cff..2277c86d09ba919f3d3bea035639ceb2177f5b67 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -78,8 +78,8 @@ Proof.
   iPoseProof (Hiter Hinv) as "H". clear Hiter.
   destruct n as [|n].
   - iApply fupd_plainly_mask_empty. iMod "H" as %?; auto.
-  - iPoseProof (step_fupdN_mono _ _ _ _ (|={⊤}=> ⌜φ⌝)%I with "H") as "H'".
-    { iIntros "H". by iApply fupd_plain_mask_empty. }
+  - iDestruct (step_fupdN_wand _ _ _ _ (|={⊤}=> ⌜φ⌝)%I with "H []") as "H'".
+    { by iApply fupd_plain_mask_empty. }
     rewrite -step_fupdN_S_fupd.
     iMod (step_fupdN_plain with "H'") as "Hφ". iModIntro. iNext.
     rewrite -later_laterN laterN_later.
@@ -92,6 +92,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_mono with "Hiter").
-  iIntros (?). iMod (fupd_intro_mask' _ ∅) as "_"; auto.
+  iApply (step_fupdN_wand with "Hiter"). by iApply (fupd_mask_weaken _ _ _).
 Qed.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 775c40330652e6d4d1f624ba5fef2f56eb5291c4..6dff72c2beda6a0f28233a4e79b7c8ca52e77640 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -359,11 +359,20 @@ Section fupd_derived.
   Qed.
 
   Lemma step_fupdN_mono E1 E2 n P Q :
-    (P ⊢ Q) → (|={E1, E2}▷=>^n P) ⊢ (|={E1, E2}▷=>^n Q).
+    (P ⊢ Q) → (|={E1,E2}▷=>^n P) ⊢ (|={E1,E2}▷=>^n Q).
   Proof.
     intros HPQ. induction n as [|n IH]=> //=. rewrite IH //.
   Qed.
 
+  Lemma step_fupdN_wand E1 E2 n P Q :
+    (|={E1,E2}▷=>^n P) -∗ (P -∗ Q) -∗ (|={E1,E2}▷=>^n Q).
+  Proof.
+    apply wand_intro_l. induction n as [|n IH]=> /=.
+    { by rewrite wand_elim_l. }
+    rewrite -IH -fupd_frame_l later_sep -fupd_frame_l.
+    by apply sep_mono; first apply later_intro.
+  Qed.
+
   Lemma step_fupdN_S_fupd n E P:
     (|={E, ∅}▷=>^(S n) P) ⊣⊢ (|={E, ∅}▷=>^(S n) |={E}=> P).
   Proof.