diff --git a/iris/base_logic/lib/fancy_updates.v b/iris/base_logic/lib/fancy_updates.v
index 6d292168ce30647a7108960aea39b0b236a76c31..b254a4f42370d65f2fc3aeedfaa21438cb271eef 100644
--- a/iris/base_logic/lib/fancy_updates.v
+++ b/iris/base_logic/lib/fancy_updates.v
@@ -99,6 +99,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.
+  iIntros (Hinv). iMod (Hiter Hinv) as "Hiter". by iApply fupd_mask_weaken.
 Qed.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index c78f6f5d0f02b1d8d7c4c4a5ec1d3aa8ab1c5984..0e365c2eec70afd318563db40a88de7752a3642e 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -58,6 +58,7 @@ Fixpoint step_fupdN {PROP : bi} `{FUpd PROP} (n : nat) (Eo Ei : coPset)
 where "|={ Eo } [ Ei ]â–·=>^ n P" := (step_fupdN n Eo Ei P) : bi_scope.
 Arguments step_fupdN {_ _} !_%nat_scope _ _ _%I.
 Instance: Params (@step_fupdN) 3 := {}.
+Typeclasses Opaque step_fupdN.
 
 Notation "P ={ Eo } [ Ei ]▷=∗^ n Q" := (P -∗ |={Eo}[Ei]▷=>^n Q)%I : bi_scope.
 Notation "P ={ Eo } [ Ei ]▷=∗^ n Q" := (P -∗ |={Eo}[Ei]▷=>^n Q) (only parsing) : stdpp_scope.
@@ -483,6 +484,14 @@ Section fupd_derived.
     by rewrite IH -step_fupd_intro // -bi.later_intro.
   Qed.
 
+  Lemma step_fupdN_combine E1 E2 E3 n P Q:
+    (|={E1}[E2]▷=>^n P) -∗ (|={E2}[E3]▷=>^n Q) -∗ (|={E1}[E3]▷=>^n P ∗ Q).
+  Proof.
+    apply wand_intro_r. induction n as [|n IH]=>//=.
+    by rewrite -IH -(fupd_trans E1 E2 E3) fupd_frame_r fupd_frame_l -later_sep
+                   -(fupd_trans E3 E2 E1) fupd_frame_l fupd_frame_r.
+  Qed.
+
   Global Instance step_fupdN_ne n Eo Ei :
     NonExpansive (step_fupdN (PROP:=PROP) n Eo Ei).
   Proof. induction n; solve_proper. Qed.
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index 895c7b5920aafef141723e064ccfbf2b2d8d4ba2..bc8dc11e3cfa2259ee834d2156fa525536cee33d 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -33,8 +33,8 @@ Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (?) "Hσ H".
   rewrite (val_stuck e1 σ1 κ e2 σ2 efs) //.
   iMod ("H" $! σ1 stepcnt with "Hσ") as "(_ & H)". iModIntro.
-  iApply (step_fupdN_wand with "[H]"); first by iApply ("H" with "[//]").
-  iIntros ">H". by rewrite Nat.add_comm big_sepL2_replicate_r.
+  iMod ("H" with "[//]") as ">H".
+  by rewrite Nat.add_comm big_sepL2_replicate_r.
 Qed.
 
 Lemma wptp_step s es1 es2 κ κs σ1 stepcnt σ2 Φs nt :
@@ -45,12 +45,12 @@ Lemma wptp_step s es1 es2 κ κs σ1 stepcnt σ2 Φs nt :
          wptp s es2 (Φs ++ replicate nt' fork_post).
 Proof.
   iIntros (Hstep) "Hσ Ht".
-  destruct Hstep as [e1' σ1' e2' σ2' efs t2' t3 Hstep]; simplify_eq/=.
+  destruct Hstep as [e1' σ1' e2' σ2' efs t2' t3 Hstep]; simplify_eq.
   iDestruct (big_sepL2_app_inv_l with "Ht") as (Φs1 Φs2 ->) "[? Ht]".
   iDestruct (big_sepL2_cons_inv_l with "Ht") as (Φ Φs3 ->) "[Ht ?]".
   iExists _. iMod (wp_step with "Hσ Ht") as "H"; first done. iModIntro.
-  iApply (step_fupdN_wand with "H"). iIntros ">($ & He2 & Hefs) !>".
-  rewrite -(assoc_L app) -app_comm_cons. iFrame.
+  iMod "H" as ">($ & He2 & Hefs)".
+  rewrite -(assoc_L app) -app_comm_cons. by iFrame.
 Qed.
 
 Lemma wptp_steps s n es1 es2 κs κs' σ1 stepcnt σ2 Φs nt :
@@ -61,17 +61,17 @@ Lemma wptp_steps s n es1 es2 κs κs' σ1 stepcnt σ2 Φs nt :
     wptp s es2 (Φs ++ replicate nt' fork_post).
 Proof.
   revert nt es1 es2 κs κs' σ1 stepcnt σ2 Φs.
-  induction n as [|n IH]=> nt es1 es2 κs κs' σ1 stepcnt σ2 Φs /=.
+  induction n as [|n IH]=> nt es1 es2 κs κs' σ1 stepcnt σ2 Φs.
   { inversion_clear 1; iIntros "? ?"; iExists 0=> /=.
     rewrite Nat.add_0_r right_id_L. iFrame. by iApply fupd_intro_mask'. }
   iIntros (Hsteps) "Hσ He". inversion_clear Hsteps as [|?? [t1' σ1']].
-  rewrite -(assoc_L (++)) step_fupdN_plus plus_n_Sm.
+  rewrite -(assoc_L (++)). simpl steps_sum. rewrite -plus_Sn_m step_fupdN_plus.
   iDestruct (wptp_step with "Hσ He") as (nt') ">H"; first eauto; simplify_eq.
-  iModIntro. iApply step_fupdN_S_fupd. iApply (step_fupdN_wand with "H").
-  iIntros ">(Hσ & He)". iMod (IH with "Hσ He") as "IH"; first done. iModIntro.
-  iApply (step_fupdN_wand with "IH"). iIntros ">IH".
-  iDestruct "IH" as (nt'') "[??]".
-  rewrite -Nat.add_assoc -(assoc_L app) -replicate_plus. by eauto with iFrame.
+  iModIntro. iApply step_fupdN_S_fupd. iMod "H" as ">(Hσ & He)".
+  iMod (IH with "Hσ He") as "IH"; first done. iModIntro.
+  iMod "IH". iMod "IH" as (nt'') "[??]".
+  rewrite -Nat.add_assoc -(assoc_L app) -replicate_plus plus_Snm_nSm.
+  by eauto with iFrame.
 Qed.
 
 Lemma wp_not_stuck κs nt e σ stepcnt Φ :
@@ -92,8 +92,7 @@ Lemma wptp_strong_adequacy Φs κs' s n es1 es2 κs σ1 stepcnt σ2 nt:
     [∗ list] e;Φ ∈ es2;Φs ++ replicate nt' fork_post, from_option Φ True (to_val e).
 Proof.
   iIntros (Hstep) "Hσ He". iMod (wptp_steps with "Hσ He") as "Hwp"; first done.
-  iModIntro. iApply (step_fupdN_wand with "Hwp").
-  iMod 1 as (nt') "(Hσ & Ht)"; simplify_eq/=.
+  iModIntro. iMod "Hwp". iMod "Hwp" as (nt') "(Hσ & Ht)" .
   iMod (fupd_plain_keep_l ⊤
     ⌜ ∀ e2, s = NotStuck → e2 ∈ es2 → not_stuck e2 σ2 ⌝%I
     (state_interp σ2 (n + stepcnt) κs' (nt + nt') ∗
@@ -105,8 +104,7 @@ Proof.
     iDestruct (big_sepL2_cons_inv_l with "Hwp") as (Φ Φs3 ->) "[Hwp ?]".
     iMod (wp_not_stuck with "Hσ Hwp") as "$"; auto. }
   iExists _. iSplitR; first done. iFrame "Hσ".
-  iApply big_sepL2_fupd.
-  iApply (big_sepL2_impl with "Hwp").
+  iApply big_sepL2_fupd. iApply (big_sepL2_impl with "Hwp").
   iIntros "!#" (? e Φ ??) "Hwp".
   destruct (to_val e) as [v2|] eqn:He2'; last done.
   apply of_to_val in He2' as <-. iApply (wp_value_inv' with "Hwp").
@@ -162,8 +160,7 @@ Proof.
   iAssert (|={∅}▷=>^(steps_sum steps_per_step 0 n) |={∅}=> ⌜φ⌝)%I
     with "[-]" as "H"; last first.
   { destruct steps_sum=>//. by iApply step_fupdN_S_fupd. }
-  iApply (step_fupdN_wand with "H").
-  iMod 1 as (nt' ?) "(Hσ & Hval) /=".
+  iMod "H". iMod "H" as (nt' ?) "(Hσ & Hval)".
   iDestruct (big_sepL2_app_inv_r with "Hval") as (es' t2' ->) "[Hes' Ht2']".
   iDestruct (big_sepL2_length with "Ht2'") as %Hlen2.
   rewrite replicate_length in Hlen2; subst.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 40018d442bc32d8fc83797a59093af72f5467b69..ea4b589ed68ace120b5445765bb8d97bd092a5c2 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -119,8 +119,7 @@ Proof.
   iMod ("H" with "[$]") as "[% H]".
   iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
   iMod ("H" $! _ _ _ with "[//]") as "H". iIntros "!> !>".  iMod "H". iModIntro.
-  iApply (step_fupdN_wand with "[H]"); first by iApply "H".
-  iIntros ">($ & H & Hefs)". iMod "Hclose" as "_". iModIntro. iSplitR "Hefs".
+  iMod "H" as ">($ & H & Hefs)". iMod "Hclose" as "_". iModIntro. iSplitR "Hefs".
   - iApply ("IH" with "[//] H HΦ").
   - iApply (big_sepL_impl with "Hefs"); iIntros "!>" (k ef _).
     iIntros "H". iApply ("IH" with "[] H"); auto.
@@ -143,8 +142,7 @@ Proof.
   { by iDestruct "H" as ">>> $". }
   iIntros (σ1 stepcnt κ κs n) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
   iModIntro. iIntros (e2 σ2 efs Hstep).
-  iApply (step_fupdN_wand with "[H]"); first by iApply ("H" with "[//]").
-  iIntros ">(Hσ & H & Hefs)". destruct s.
+  iMod ("H" with "[//]") as ">(Hσ & H & Hefs)". destruct s.
   - rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
     + iDestruct "H" as ">> $". by iFrame.
     + iMod ("H" $! _ _ [] with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ? & ?).
@@ -174,9 +172,9 @@ Proof.
   iIntros "!>" (e2 σ2 efs Hstep). iMod ("H" $! e2 σ2 efs with "[% //]") as "H".
   iIntros "!>!>". iMod "H". iMod "HR". iModIntro. iClear "Hn".
   revert n Hn. generalize (steps_per_step stepcnt)=>n0 n Hn.
-  iInduction n as [|n] "IH" forall (n0 Hn).
-  - iApply (step_fupdN_wand with "H"). iIntros ">($ & Hwp & $)". iMod "HR".
-    iModIntro. iApply (wp_strong_mono with "Hwp"); [done|set_solver|].
+  iInduction n as [|n] "IH" forall (n0 Hn)=>/=.
+  - iMod "H" as ">($ & Hwp & $)". iMod "HR". iModIntro.
+    iApply (wp_strong_mono with "Hwp"); [done|set_solver|].
     iIntros (v) "HΦ {$HQ}". by iApply "HΦ".
   - destruct n0 as [|n0]; [lia|]=>/=. iMod "HR". iMod "H". iIntros "!> !>".
     iMod "HR". iMod "H". iModIntro. iApply ("IH" with "[] HQ HR H").
@@ -208,8 +206,7 @@ Proof.
   iIntros (e2 σ2 efs Hstep).
   destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
   iMod ("H" $! e2' σ2 efs with "[//]") as "H". iIntros "!>!>".
-  iMod "H". iModIntro. iApply (step_fupdN_wand with "H"). iIntros "H".
-  iMod "H" as "($ & H & $)". iModIntro. by iApply "IH".
+  iMod "H". iModIntro. iMod "H" as ">($ & H & $)". by iApply "IH".
 Qed.
 
 Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ :
@@ -224,8 +221,7 @@ Proof.
   { destruct s; eauto using reducible_fill_inv. }
   iIntros (e2 σ2 efs Hstep).
   iMod ("H" $! _ _ _ with "[]") as "H"; first eauto using fill_step.
-  iIntros "!> !>". iMod "H". iModIntro. iApply (step_fupdN_wand with "H").
-  iIntros "H". iMod "H" as "($ & H & $)". iModIntro. by iApply "IH".
+  iIntros "!> !>". iMod "H". iModIntro. iMod "H" as ">($ & H & $)". by iApply "IH".
 Qed.
 
 (** * Derived rules *)
diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index f77d3a1481b23efc716ff4f50e5125362ce0bbdd..46f2713441c52f03d802abf80ff1a3330d245829 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -195,6 +195,13 @@ Proof.
     fupd_frame_r wand_elim_r fupd_trans.
 Qed.
 
+Global Instance elim_modal_step_fupdN `{!BiFUpd PROP} p E1 E2 n P Q :
+  ElimModal True p false (|={E1}[E2]â–·=>^n P) P (|={E1}[E2]â–·=>^n Q) Q.
+Proof.
+  by rewrite /ElimModal intuitionistically_if_elim /=
+             (step_fupdN_wand _ _ _ _ Q) wand_elim_l.
+Qed.
+
 Global Instance add_modal_bupd `{!BiBUpd PROP} P Q : AddModal (|==> P) P (|==> Q).
 Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.