diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index 654c777484cb108fd1f3793fcacff3b8c1fdb045..6da24be014129ca9e37e28552d830f3141b40363 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -20,9 +20,8 @@ Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
   adequate e σ φ.
 Proof.
   intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
-  iVs (auth_alloc to_heap ownP heapN _ σ with "[Hσ]") as (γ) "[Hh _]".
+  iVs (auth_alloc to_heap _ heapN _ σ with "[Hσ]") as (γ) "[Hh _]";[|by iNext|].
   { exact: to_heap_valid. }
-  { by iNext. }
   set (Hheap := HeapG _ _ _ γ).
   iApply (Hwp _). by rewrite /heap_ctx.
 Qed.