diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 324dfa1da32e82643b9d8e88263e2094ad6b3f68..05f0a8f3b3a0e01cbeaa1549e446a9734ab50e2b 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -223,13 +223,13 @@ Implicit Types l : loc.
 induction directly, but this demonstrates that we can state the expected
 reasoning principle for recursive functions, without any visible â–·. *)
 Lemma wp_rec_löb s E f x e Φ Ψ :
-  □ ((∀ v, Ψ v -∗ WP (rec: f x := e)%V v @ s; E {{ Φ }}) -∗
+  □ ( □ (∀ v, Ψ v -∗ WP (rec: f x := e)%V v @ s; E {{ Φ }}) -∗
      ∀ v, Ψ v -∗ WP (subst' x v (subst' f (rec: f x := e) e)) @ s; E {{ Φ }}) -∗
   ∀ v, Ψ v -∗ WP (rec: f x := e)%V v @ s; E {{ Φ }}.
 Proof.
   iIntros "#Hrec". iLöb as "IH". iIntros (v) "HΨ".
   iApply lifting.wp_pure_step_later; first done.
-  iNext. iApply ("Hrec" with "[] HΨ"). iIntros (w) "HΨ".
+  iNext. iApply ("Hrec" with "[] HΨ"). iIntros "!#" (w) "HΨ".
   iApply ("IH" with "HΨ").
 Qed.