diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 2c4a5818f9907c8b74a56a262742206cc047fa69..37535edcd8b266485255b59f3d1be22eee7b0fac 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -63,11 +63,10 @@ Lemma step_fupdN_soundness `{invPreG Σ} φ n :
   (∀ `{Hinv: invG Σ}, (|={⊤, ∅}▷=>^n |={⊤, ∅}=> ⌜ φ ⌝ : iProp Σ)%I) →
   φ.
 Proof.
-  iIntros (Hiter).
-  eapply (soundness (M:=iResUR Σ) _  (S (S n))).
-  eapply (fupd_plain_soundness ⊤); first by apply _.
-  intros Hinv. rewrite -/sbi_laterN.
-  iPoseProof (Hiter Hinv) as "H".
+  intros Hiter.
+  apply (soundness (M:=iResUR Σ) _  (S (S n))); simpl.
+  apply (fupd_plain_soundness ⊤ _).
+  intros Hinv. iPoseProof (Hiter Hinv) as "H".
   destruct n as [|n].
   - rewrite //=. iPoseProof (fupd_plain_strong with "H") as "H'".
     do 2 iMod "H'"; iModIntro; auto.