diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 855e5c26b7256d52b1cfa2fa32a58ff549cb2a8f..425839b1c919152cf4cca944fa236ad72cadda8b 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -86,7 +86,7 @@ Notation "'withcont:' k1 ':' e1 'cont:' k2 xl := e2" :=
   ((Lam (@cons binder k1%RustB nil) e1%E) [Rec k2%RustB ((fun _ : eq k1%RustB k2%RustB => xl%RustB) eq_refl) e2%E])
   (only parsing, at level 151, k1, k2, xl at level 1, e2 at level 150) : expr_scope.
 
-Notation "'call:' f args → k" := (f (@cons expr (λ: ["_r"], Endlft ;; k ["_r"])%V args))%E
+Notation "'call:' f args → k" := (f (@cons expr (λ: ["_r"], Endlft ;; k ["_r"]) args))%E
   (only parsing, at level 102, f, args, k at level 1) : expr_scope.
 Notation "'letcall:' x := f args 'in' e" :=
   (letcont: "_k" [ x ] := e in call: f args → "_k")%E
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 73e0cd6f73cb5e33d8b9ab8ff40992117d4203c0..58955702511792aa470d5930ab1328c86eb0ce68 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -181,7 +181,7 @@ Ltac solve_to_val :=
   match goal with
   | |- to_val ?e = Some ?v =>
      let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v);
-     apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity
+     apply W.to_val_Some; simpl; unfold W.to_expr; unlock; reflexivity
   | |- is_Some (to_val ?e) =>
      let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e')));
      apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
diff --git a/theories/typing/function.v b/theories/typing/function.v
index ca51e24e35fe73c8252265a1893e28b9bc900593..a2cfc11c399dfeeb483f537bd1ae00e04ef692d6 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -8,14 +8,14 @@ Set Default Proof Using "Type".
 Section fn.
   Context `{typeG Σ} {A : Type} {n : nat}.
 
-  Record fn_params := FP' { fp_tys : vec type n; fp_ty : type; fp_E : elctx }.
+  Record fn_params := FP' { fp_tys : vec type n; fp_ty : type; fp_E : lft → elctx }.
 
   Program Definition fn (fp : A → fn_params) : type :=
     {| st_own tid vl := (∃ fb kb xb e H,
          ⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
-         ▷ ∀ (x : A) (k : val) (xl : vec val (length xb)),
-            â–¡ typed_body (fp x).(fp_E) []
-                         [k◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+         ▷ ∀ (x : A) (ϝ : lft) (k : val) (xl : vec val (length xb)),
+            □ typed_body ((fp x).(fp_E)  ϝ) [ϝ ⊑ []]
+                         [k◁cont([ϝ ⊑ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
                          (zip_with (TCtx_hasty ∘ of_val) xl
                                    (box <$> (vec_to_list (fp x).(fp_tys))))
                          (subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
@@ -29,7 +29,7 @@ Section fn.
   Definition fn_params_rel (ty_rel : relation type) : relation fn_params :=
     λ fp1 fp2,
       Forall2 ty_rel fp2.(fp_tys) fp1.(fp_tys) ∧ ty_rel fp1.(fp_ty) fp2.(fp_ty) ∧
-      fp1.(fp_E) = fp2.(fp_E).
+      pointwise_relation lft eq fp1.(fp_E) fp2.(fp_E).
 
   Global Instance fp_tys_proper R :
     Proper (flip (fn_params_rel R) ==> (Forall2 R : relation (vec _ _))) fp_tys.
@@ -43,11 +43,12 @@ Section fn.
   Proof. intros ?? HR. apply HR. Qed.
 
   Global Instance fp_E_proper R :
-    Proper (fn_params_rel R ==> eq) fp_E.
-  Proof. intros ?? HR. apply HR. Qed.
+    Proper (fn_params_rel R ==> eq ==> eq) fp_E.
+  Proof. intros ?? HR ??->. apply HR. Qed.
 
   Global Instance FP_proper R :
-    Proper (flip (Forall2 R : relation (vec _ _)) ==> R ==> eq ==> fn_params_rel R) FP'.
+    Proper (flip (Forall2 R : relation (vec _ _)) ==> R ==>
+            pointwise_relation lft eq ==> fn_params_rel R) FP'.
   Proof. by split; [|split]. Qed.
 
   Global Instance fn_type_contractive n' :
@@ -59,11 +60,10 @@ Section fn.
     (* TODO: 'f_equiv' is slow here because reflexivity is slow. *)
     (* The clean way to do this would be to have a metric on type contexts. Oh well. *)
     intros tid vl. unfold typed_body.
-    do 12 f_equiv. f_contractive. do 17 (apply Hfp || f_equiv).
-    - f_equiv. apply Hfp.
+    do 12 f_equiv. f_contractive. do 16 ((eapply fp_E_proper; try reflexivity) || exact: Hfp || f_equiv).
     - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
       rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat (apply Hfp || f_equiv).
-    - rewrite /tctx_interp !big_sepL_zip_with /=. do 3 f_equiv.
+    - rewrite /tctx_interp !big_sepL_zip_with /=. do 4 f_equiv.
       cut (∀ n tid p i, Proper (dist n ==> dist n)
         (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I).
       { intros Hprop. apply Hprop, list_fmap_ne; last first.
@@ -132,49 +132,56 @@ Section typing.
   Context `{typeG Σ}.
 
   Lemma fn_subtype {A n} E0 L0 (fp fp' : A → fn_params n) :
-    (∀ x, elctx_incl E0 L0 (fp' x).(fp_E) (fp x).(fp_E)) →
-    (∀ x, Forall2 (subtype (E0 ++ (fp' x).(fp_E)) L0)
-                  (fp' x).(fp_tys) (fp x).(fp_tys)) →
-    (∀ x, subtype (E0 ++ (fp' x).(fp_E)) L0 (fp x).(fp_ty) (fp' x).(fp_ty)) →
+    (∀ x ϝ, let EE := E0 ++ (fp' x).(fp_E) ϝ in
+            elctx_sat EE L0 ((fp x).(fp_E) ϝ) ∧
+            Forall2 (subtype EE L0) (fp' x).(fp_tys) (fp x).(fp_tys) ∧
+            subtype EE L0 (fp x).(fp_ty) (fp' x).(fp_ty)) →
     subtype E0 L0 (fn fp) (fn fp').
   Proof.
-    intros HE Htys Hty. apply subtype_simple_type=>//= _ vl.
-    iIntros "#HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
+    intros Hcons. apply subtype_simple_type=>//= qL. iIntros "HL0".
+    (* We massage things so that we can throw away HL0 before going under the box. *)
+    iAssert (∀ x ϝ, let EE := E0 ++ (fp' x).(fp_E) ϝ in □ (elctx_interp EE -∗
+                 elctx_interp ((fp x).(fp_E) ϝ) ∗
+                 ([∗ list] tys ∈ (zip (fp' x).(fp_tys) (fp x).(fp_tys)), type_incl (tys.1) (tys.2)) ∗
+                 type_incl (fp x).(fp_ty) (fp' x).(fp_ty)))%I as "#Hcons".
+    { iIntros (x ϝ). destruct (Hcons x ϝ) as (HE &Htys &Hty). clear Hcons.
+      iDestruct (HE with "HL0") as "#HE".
+      iDestruct (subtype_Forall2_llctx with "HL0") as "#Htys"; first done.
+      iDestruct (Hty with "HL0") as "#Hty".
+      iClear "∗". iIntros "!# #HEE".
+      iSplit; last iSplit.
+      - by iApply "HE".
+      - by iApply "Htys".
+      - by iApply "Hty". }
+    iClear "∗". clear Hcons. iIntros "!# #HE0 * Hf".
+    iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
     iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iNext.
-    rewrite /typed_body. iIntros (x k xl) "!# * #LFT Htl HE HL HC HT".
-    iDestruct (elctx_interp_persist with "HE") as "#HEp".
-    iMod (HE with "HE0 HL0 HE") as (qE') "[HE' Hclose]". done.
-    iApply ("Hf" with "LFT Htl HE' HL [HC Hclose] [HT]").
-    - iIntros "HE'". unfold cctx_interp. iIntros (elt) "Helt".
+    rewrite /typed_body. iIntros (x ϝ k xl) "!# * #LFT #HE' Htl HL HC HT".
+    iDestruct ("Hcons" with "[$]") as "#(HE & Htys & Hty)".
+    iApply ("Hf" with "LFT HE Htl HL [HC] [HT]").
+    - unfold cctx_interp. iIntros (elt) "Helt".
       iDestruct "Helt" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
-      iMod ("Hclose" with "HE'") as "HE".
-      iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
+      unfold cctx_elt_interp.
       iApply ("HC" $! (_ ◁cont(_, _)%CC) with "[%] Htl HL [> -]").
       { by apply elem_of_list_singleton. }
       rewrite /tctx_interp !big_sepL_singleton /=.
       iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
-      assert (Hst : subtype (E0 ++ (fp' x).(fp_E)) L0
-                            (box (fp x).(fp_ty)) (box (fp' x).(fp_ty)))
-        by by rewrite ->Hty.
-      iDestruct (Hst with "[HE0 HEp] HL0") as "(_ & Hty & _)".
-      { rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
-      by iApply "Hty".
-    - rewrite /tctx_interp
-         -(fst_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
-         -{1}(snd_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
+      iDestruct (box_type_incl with "[$Hty]") as "(_ & #Hincl & _)".
+      by iApply "Hincl".
+    - iClear "Hf". rewrite /tctx_interp
+         -{2}(fst_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
+         -{2}(snd_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
          !zip_with_fmap_r !(zip_with_zip (λ _ _, (_ ∘ _) _ _)) !big_sepL_fmap.
-      iApply big_sepL_impl. iSplit; last done. iIntros "{HT}!#".
+      iApply big_sepL_impl. iSplit; last done. iIntros "{HT Hty}!#".
       iIntros (i [p [ty1' ty2']]) "#Hzip H /=".
       iDestruct "H" as (v) "[? Hown]". iExists v. iFrame.
       rewrite !lookup_zip_with.
       iDestruct "Hzip" as %(? & ? & ([? ?] & (? & Hty'1 &
         (? & Hty'2 & [=->->])%bind_Some)%bind_Some & [=->->->])%bind_Some)%bind_Some.
-      eapply Forall2_lookup_lr in Htys; try done.
-      assert (Hst : subtype (E0 ++ (fp' x).(fp_E)) L0 (box ty2') (box ty1'))
-        by by rewrite ->Htys.
-      iDestruct (Hst with "[] []") as "(_ & #Ho & _)"; [ |done|].
-      { rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
-      by iApply "Ho".
+      iDestruct (big_sepL_lookup with "Htys") as "#Hty".
+      { rewrite lookup_zip_with /=. erewrite Hty'2. simpl. by erewrite Hty'1. }
+      iDestruct (box_type_incl with "[$Hty]") as "(_ & #Hincl & _)".
+      by iApply "Hincl".
   Qed.
 
   (* This proper and the next can probably not be inferred, but oh well. *)
@@ -182,8 +189,9 @@ Section typing.
     Proper (pointwise_relation A (fn_params_rel (n:=n) (subtype E0 L0)) ==>
             subtype E0 L0) fn.
   Proof.
-    intros fp1 fp2 Hfp. apply fn_subtype=>x; destruct (Hfp x) as (Htys & Hty & HE).
-    - by rewrite HE.
+    intros fp1 fp2 Hfp. apply fn_subtype=>x ϝ. destruct (Hfp x) as (Htys & Hty & HE).
+    split; last split.
+    - rewrite (HE ϝ). apply elctx_sat_app_weaken_l, elctx_sat_refl.
     - eapply Forall2_impl; first eapply Htys. intros ??.
       eapply subtype_weaken; last done. by apply submseteq_inserts_r.
     - eapply subtype_weaken, Hty; last done. by apply submseteq_inserts_r.
@@ -193,12 +201,12 @@ Section typing.
     Proper (pointwise_relation A (fn_params_rel (n:=n) (eqtype E0 L0)) ==>
             eqtype E0 L0) fn.
   Proof.
-    intros fp1 fp2 Hfp. split; eapply fn_subtype=>x; destruct (Hfp x) as (Htys & Hty & HE).
-    - by rewrite HE.
+    intros fp1 fp2 Hfp. split; eapply fn_subtype=>x ϝ; destruct (Hfp x) as (Htys & Hty & HE); (split; last split).
+    - rewrite (HE ϝ). apply elctx_sat_app_weaken_l, elctx_sat_refl.
     - eapply Forall2_impl; first eapply Htys. intros t1 t2 Ht.
       eapply subtype_weaken; last apply Ht; last done. by apply submseteq_inserts_r.
     - eapply subtype_weaken; last apply Hty; last done. by apply submseteq_inserts_r.
-    - by rewrite HE.
+    - rewrite (HE ϝ). apply elctx_sat_app_weaken_l, elctx_sat_refl.
     - symmetry in Htys. eapply Forall2_impl; first eapply Htys. intros t1 t2 Ht.
       eapply subtype_weaken; last apply Ht; last done. by apply submseteq_inserts_r.
     - eapply subtype_weaken; last apply Hty; last done. by apply submseteq_inserts_r.
@@ -207,28 +215,29 @@ Section typing.
   Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 fp :
     subtype E0 L0 (fn (n:=n) fp) (fn (fp ∘ σ)).
   Proof.
-    apply subtype_simple_type=>//= _ vl.
-    iIntros "_ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
+    apply subtype_simple_type=>//= qL.
+    iIntros "_ !# _ * Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
     iExists fb, kb, xb, e, _. iSplit. done. iSplit. done.
     rewrite /typed_body. iNext. iIntros "*". iApply "Hf".
   Qed.
 
-  Lemma type_call' {A} E L T p (ps : list path)
-                         (fp : A → fn_params (length ps)) k x :
-    elctx_sat E L (fp x).(fp_E) →
+  Lemma type_call' {A} E L T p (κs : list lft) (ps : list path)
+                         (fp : A → fn_params (length ps)) (k : val) x :
+    Forall (lctx_lft_alive E L) κs →
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ κ) <$> κs)%EL ++ E) L ((fp x).(fp_E) ϝ)) →
     typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ box (fp x).(fp_ty)) :: T)]
                ((p ◁ fn fp) ::
                 zip_with TCtx_hasty ps (box <$> (vec_to_list (fp x).(fp_tys))) ++
                 T)
                (call: p ps → k).
   Proof.
-    iIntros (HE tid qE) "#LFT Htl HE HL HC".
-    rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
+    iIntros (Hκs HE tid) "#LFT #HE Htl HL HC (Hf & Hargs & HT)".
     wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
-    iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = k⌝):::
+    iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = (λ: ["_r"], (#() ;; #()) ;; k ["_r"])%V⌝):::
                vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ box ty)) (fp x).(fp_tys))%I
             with "[Hargs]"); first wp_done.
-    - rewrite /= big_sepL_cons. iSplitR "Hargs"; first by iApply wp_value'.
+    - rewrite /= big_sepL_cons. iSplitR "Hargs".
+      { simpl. iApply wp_value; last done. solve_to_val. }
       clear dependent k p.
       rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
               (zip_with_zip (λ e ty, (e, _))) zip_with_zip !big_sepL_fmap.
@@ -240,16 +249,25 @@ Section typing.
       iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl. revert vl fp HE.
       rewrite <-EQl=>vl fp HE. iApply wp_rec; try done.
       { rewrite -fmap_cons Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
-      { rewrite -fmap_cons -(subst_v_eq (fb::kb::xb) (_:::k:::vl)) //. }
-      iNext. iSpecialize ("Hf" $! x k vl).
-      iMod (HE with "HE HL") as (q') "[HE' Hclose]"; first done.
-      iApply ("Hf" with "LFT Htl HE' [] [HC Hclose HT]").
-      + by rewrite /llctx_interp big_sepL_nil.
-      + iIntros "HE'". iApply fupd_cctx_interp. iMod ("Hclose" with "HE'") as "[HE HL]".
-        iSpecialize ("HC" with "HE"). iModIntro. iIntros (y) "IN".
-        iDestruct "IN" as %->%elem_of_list_singleton. iIntros (args) "Htl _ Hret".
+      { rewrite -fmap_cons -(subst_v_eq (fb::kb::xb) (_:::_:::vl)) //. }
+      iNext. iMod (lft_create with "LFT") as (ϝ) "[Htk #Hinh]"; first done.
+      iSpecialize ("Hf" $! x ϝ _ vl).
+      iDestruct (HE ϝ with "HL") as "#HE'".
+      iMod (lctx_lft_alive_list with "LFT [# $HE //] HL") as "[#HEE Hclose]"; [done..|].
+      iApply ("Hf" with "LFT [>] Htl [Htk] [HC HT Hclose]").
+      + iApply "HE'". iFrame "#". auto.
+      + iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.
+        iFrame "#∗".
+      + iIntros (y) "IN". iDestruct "IN" as %->%elem_of_list_singleton.
+        iIntros (args) "Htl [HL _] Hret". inv_vec args=>r.
+        iDestruct "HL" as  (κ') "(EQ & Htk & _)". iDestruct "EQ" as %EQ.
+        rewrite /= left_id in EQ. subst κ'. simpl. wp_rec. wp_bind Endlft.
+        iSpecialize ("Hinh" with "Htk").
+        iApply (wp_mask_mono (↑lftN)); first done.
+        iApply (wp_step_fupd with "Hinh"); [set_solver+..|]. wp_seq.
+        iIntros "#Htok !>". wp_seq. iMod ("Hclose" with "Htok") as "HL".
         iSpecialize ("HC" with "[]"); first by (iPureIntro; apply elem_of_list_singleton).
-        iApply ("HC" $! args with "Htl HL").
+        iApply ("HC" $! [#r] with "Htl HL").
         rewrite tctx_interp_singleton tctx_interp_cons. iFrame.
       + rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
                 (zip_with_zip (λ v ty, (v, _))) zip_with_zip !big_sepL_fmap.
@@ -259,14 +277,15 @@ Section typing.
   Lemma type_call {A} x E L C T T' T'' p (ps : list path)
                         (fp : A → fn_params (length ps)) k :
     (p ◁ fn fp)%TC ∈ T →
-    elctx_sat E L (fp x).(fp_E) →
+    Forall (lctx_lft_alive E L) (L.*1) →
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ κ) <$> (L.*1))%EL ++ E) L ((fp x).(fp_E) ϝ)) →
     tctx_extract_ctx E L (zip_with TCtx_hasty ps
                                    (box <$> vec_to_list (fp x).(fp_tys))) T T' →
     (k ◁cont(L, T''))%CC ∈ C →
     (∀ ret : val, tctx_incl E L ((ret ◁ box (fp x).(fp_ty))::T') (T'' [# ret])) →
     typed_body E L C T (call: p ps → k).
   Proof.
-    intros Hfn HE HTT' HC HT'T''.
+    intros Hfn HL HE HTT' HC HT'T''.
     rewrite -typed_body_mono /flip; last done; first by eapply type_call'.
     - etrans. eapply (incl_cctx_incl _ [_]); first by intros ? ->%elem_of_list_singleton.
       apply cctx_incl_cons_match; first done. intros args. by inv_vec args.
@@ -278,13 +297,14 @@ Section typing.
                         (fp : A → fn_params (length ps)) b e :
     Closed (b :b: []) e → Closed [] p → Forall (Closed []) ps →
     (p ◁ fn fp)%TC ∈ T →
-    elctx_sat E L (fp x).(fp_E) →
+    Forall (lctx_lft_alive E L) (L.*1) →
+    (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ κ) <$> (L.*1))%EL ++ E) L ((fp x).(fp_E) ϝ)) →
     tctx_extract_ctx E L (zip_with TCtx_hasty ps
                                    (box <$> vec_to_list (fp x).(fp_tys))) T T' →
     (∀ ret : val, typed_body E L C ((ret ◁ box (fp x).(fp_ty))::T') (subst' b ret e)) -∗
     typed_body E L C T (letcall: b := p ps in e).
   Proof.
-    iIntros (?? Hpsc ???) "He".
+    iIntros (?? Hpsc ????) "He".
     iApply (type_cont_norec [_] _ (λ r, (r!!!0 ◁ box (fp x).(fp_ty)) :: T')%TC).
     - (* TODO : make [solve_closed] work here. *)
       eapply is_closed_weaken; first done. set_solver+.
@@ -295,8 +315,8 @@ Section typing.
         intros. eapply Is_true_eq_true, is_closed_weaken=>//. set_solver+.
     - iIntros (k).
       (* TODO : make [simpl_subst] work here. *)
-      change (subst' "_k" k (p (Var "_k" :: ps))) with
-             ((subst "_k" k p) (of_val k :: map (subst "_k" k) ps)).
+      change (subst' "_k" k (p ((λ: ["_r"], (#() ;; #()) ;; "_k" ["_r"])%E :: ps))) with
+             ((subst "_k" k p) ((λ: ["_r"], (#() ;; #()) ;; k ["_r"])%E :: map (subst "_k" k) ps)).
       rewrite is_closed_nil_subst //.
       assert (map (subst "_k" k) ps = ps) as ->.
       { clear -Hpsc. induction Hpsc=>//=. rewrite is_closed_nil_subst //. congruence. }
@@ -313,22 +333,22 @@ Section typing.
     ef = (funrec: fb argsb := e)%E →
     n = length argsb →
     Closed (fb :b: "return" :b: argsb +b+ []) e →
-    □ (∀ x (f : val) k (args : vec val (length argsb)),
-          typed_body (fp x).(fp_E) []
-                     [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+    □ (∀ x ϝ (f : val) k (args : vec val (length argsb)),
+          typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ []]
+                     [k ◁cont([ϝ ⊑ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
                      ((f ◁ fn fp) ::
                         zip_with (TCtx_hasty ∘ of_val) args
                                  (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
                      (subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
     typed_instruction_ty E L T ef (fn fp).
   Proof.
-    iIntros (-> -> Hc) "#Hbody". iIntros (tid qE) " #LFT $ $ $ #HT". iApply wp_value.
+    iIntros (-> -> Hc) "#Hbody". iIntros (tid) "#LFT _ $ $ #HT". iApply wp_value.
     { simpl. rewrite ->(decide_left Hc). done. }
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
     { simpl. rewrite decide_left. done. }
-    iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext. clear qE.
-    iIntros (x k args) "!#". iIntros (tid' qE) "_ Htl HE HL HC HT'".
-    iApply ("Hbody" with "LFT Htl HE HL HC").
+    iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext.
+    iIntros (x ϝ k args) "!#". iIntros (tid') "_ HE Htl HL HC HT'".
+    iApply ("Hbody" with "LFT HE Htl HL HC").
     rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
     by iApply sendc_change_tid.
   Qed.
@@ -338,9 +358,9 @@ Section typing.
     ef = (funrec: <> argsb := e)%E →
     n = length argsb →
     Closed ("return" :b: argsb +b+ []) e →
-    □ (∀ x k (args : vec val (length argsb)),
-        typed_body (fp x).(fp_E) []
-                   [k ◁cont([], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+    □ (∀ x ϝ k (args : vec val (length argsb)),
+        typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ []]
+                   [k ◁cont([ϝ ⊑ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
                    (zip_with (TCtx_hasty ∘ of_val) args
                              (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
                    (subst_v (BNamed "return" :: argsb) (k ::: args) e)) -∗
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index f0c218eafd5929a22018b1b9e51e270afb31d5d3..37c358ac44b8e90eafc7c2ea2dcc554cf13dd751 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -216,6 +216,27 @@ Section lft_contexts.
     iExists q''. iIntros "{$Htok}!>Htok". iApply ("Hclose" with "[> -]").
     by iApply "Hclose'".
   Qed.
+  
+  Lemma lctx_lft_alive_list κs ϝ `{!frac_borG Σ} :
+    Forall lctx_lft_alive κs →
+    ∀ (F : coPset) (qL : Qp),
+      ↑lftN ⊆ F → lft_ctx -∗ elctx_interp E -∗
+         llctx_interp L qL ={F}=∗ elctx_interp ((λ κ, ϝ ⊑ κ) <$> κs)%EL ∗
+                                   ([†ϝ] ={F}=∗ llctx_interp L qL).
+  Proof.
+    iIntros (Hκs F qL ?) "#LFT #HE". iInduction κs as [|κ κs] "IH" forall (qL Hκs).
+    { iIntros "$ !>". rewrite /elctx_interp big_sepL_nil. auto. }
+    iIntros "[HL1 HL2]". inversion Hκs as [|?? Hκ Hκs']. clear Hκs. subst.
+    iMod ("IH" with "[% //] HL2") as "[#Hκs Hclose1] {IH}".
+    iMod (Hκ with "HE HL1") as (q) "[Hκ Hclose2]"; first done.
+    iMod (bor_create with "LFT [Hκ]") as "[Hκ H†]"; first done. iApply "Hκ".
+    iDestruct (frac_bor_lft_incl _ _ q with "LFT [> Hκ]") as "#Hincl".
+    { iApply (bor_fracture with "LFT [>-]"); first done. simpl.
+      rewrite Qp_mult_1_r. done. (* FIXME: right_id? *) }
+    iModIntro. iFrame "#". iIntros "#Hϝ†".
+    iMod ("H†" with "Hϝ†") as ">Hκ". iMod ("Hclose2" with "Hκ") as "$".
+    by iApply "Hclose1".
+  Qed.
 
   (* External lifetime context satisfiability *)