diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 3db8c3525122fa1465deea31b722d8d10bf27baf..b5a608107b471e2c68a930c33212a7845d39a0e7 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -23,8 +23,8 @@ Section typing.
     Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
     (∀ k args, typed_body E L1 (CCtx_iscont k L1 _ T' :: C) (T' args)
                           (subst' kb k $ subst_v argsb (vmap of_val args) econt)) →
-    (∀ k, typed_body E (L1 ++ L2) (CCtx_iscont k L1 _ T' :: C) T (subst' kb k e2)) →
-    typed_body E (L1 ++ L2) C T (let: kb := Rec kb argsb econt in e2).
+    (∀ k, typed_body E L2 (CCtx_iscont k L1 _ T' :: C) T (subst' kb k e2)) →
+    typed_body E L2 C T (let: kb := Rec kb argsb econt in e2).
   Proof.
     iIntros (Hc1 Hc2 Hecont He2 tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
     { simpl. rewrite decide_left. done. }