diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 024f6410ae410a3aa49bed4bdcd193e6c5b7a33d..6db93b1319fba5f06b1f55b05765f98bade5ae2d 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -93,5 +93,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_weaken.
 Qed.