typing of letcont: allow picking an arbitrary local lifetime context

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. }