diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 1185a506fca4a1b23b6944e673daf9e442f9adaf..5533cb1d87a2fbcbb410f57e4533b5521e6af36c 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -130,7 +130,7 @@ Qed.
 Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
-  Nat.iter n (λ P, |={E,E'}▷=> P) (WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
+  (|={E,E'}▷=>^n WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
   iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.