diff --git a/theories/typing/adequacy.v b/theories/typing/adequacy.v
index 7b4eff80ee483898653d1b03ceab7fb97db72457..674fdaa29aac4aba04868b2e9839eda863d1f19e 100644
--- a/theories/typing/adequacy.v
+++ b/theories/typing/adequacy.v
@@ -44,17 +44,15 @@ Section type_soundness.
     { by rewrite /elctx_interp big_sepL_nil. }
     { by rewrite /llctx_interp big_sepL_nil. }
     { by rewrite tctx_interp_nil. }
-    clear Hrtc Hmain main. iIntros (main) "(Htl & _ & _ & Hmain)".
+    clear Hrtc Hmain main. iIntros (main) "(Htl & HE & HL & Hmain)".
     rewrite tctx_interp_singleton. iDestruct "Hmain" as (?) "[EQ Hmain]".
     rewrite eval_path_of_val. iDestruct "EQ" as %[= <-].
     iDestruct "Hmain" as (f k x e ?) "(EQ & % & Hmain)". iDestruct "EQ" as %[= ->].
     destruct x; try done.
     iApply (wp_rec _ _ _ _ _ _ [exit_cont]%E); [done| |by simpl_subst|iNext].
     { repeat econstructor. apply to_of_val. }
-    iApply ("Hmain" $! () exit_cont [#] tid 1%Qp with "HEAP LFT Htl [] [] []");
+    iApply ("Hmain" $! () exit_cont [#] tid 1%Qp with "HEAP LFT Htl HE HL []");
       last by rewrite tctx_interp_nil.
-    { by rewrite /elctx_interp big_sepL_nil. }
-    { by rewrite /llctx_interp big_sepL_nil. }
     iIntros "_". rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
     inv_vec args. iIntros (x) "_". by wp_seq.
   Qed.