diff --git a/theories/typing/base.v b/theories/typing/base.v
index 913b772e6d3387f3695019dae64d4574e44a815d..c69fbf5f8648e6a3024411fdc6bdf77f6e3ed8e8 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -1,3 +1,4 @@
+From lrust.lang Require Export proofmode.
 From lrust.lifetime Require Export frac_borrow.
 
 Create HintDb lrust_typing.
@@ -12,3 +13,20 @@ Create HintDb lrust_typing_merge.
 Ltac solve_typing :=
   (typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
   (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
+
+Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
+Hint Resolve
+     of_val_unlock
+     submseteq_cons submseteq_inserts_l submseteq_inserts_r
+  : lrust_typing.
+
+Hint Extern 1 (@eq nat _ (Z.to_nat _)) =>
+  (etrans; [symmetry; exact: Nat2Z.id | reflexivity]) : lrust_typing.
+Hint Extern 1 (@eq nat (Z.to_nat _) _) =>
+  (etrans; [exact: Nat2Z.id | reflexivity]) : lrust_typing.
+
+(* FIXME : I would prefer using a [Hint Resolve <-] for this, but
+   unfortunately, this is not preserved across modules. See:
+     https://coq.inria.fr/bugs/show_bug.cgi?id=5189
+   This should be fixed in the next version of Coq. *)
+Hint Extern 1 (_ ∈ _ ++ _) => apply <- @elem_of_app : lrust_typing.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 0ed4fd617819677fcd789f159dcd3c683f2ca72a..e254f5919003255fb17d7082b1236b05df6216e4 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -37,7 +37,7 @@ Section lazy_lft.
     iApply (type_assign _ (&shr{α}int)); [solve_typing..|].
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_endlft; [solve_typing..|].
-    iApply (type_delete (Π[&shr{_}_;&shr{_}_])%T); [solve_typing..|].
+    iApply (type_delete (Π[&shr{α}_;&shr{α}_])%T); [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 403ddcffdab8e1c7311c961e0f6d745deb6d7bf1..7a8d92f6003039e25e14636855b44ccc6486bfd4 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -241,9 +241,10 @@ Section typing.
     lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗ llctx_interp L qL -∗
     qκs.[lft_intersect_list κs] -∗
     tctx_elt_interp tid (p ◁ fn fp) -∗
-    ([∗ list] y ∈ zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)), tctx_elt_interp tid y) -∗
+    ([∗ list] y ∈ zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)),
+                   tctx_elt_interp tid y) -∗
     (∀ ret, na_own tid top -∗ llctx_interp L qL -∗ qκs.[lft_intersect_list κs] -∗
-             (box (fp x).(fp_ty)).(ty_own) tid [ret] -∗ 
+             (box (fp x).(fp_ty)).(ty_own) tid [ret] -∗
              WP k [of_val ret] {{ _, cont_postcondition }}) -∗
     WP (call: p ps → k) {{ _, cont_postcondition }}.
   Proof.
@@ -276,7 +277,8 @@ Section typing.
       + iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
         iInduction κs as [|κ κs] "IH"=> //=. iSplitL.
         { iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
-        iApply "IH". iAlways. iApply lft_incl_trans; first done. iApply lft_intersect_incl_r.
+        iApply "IH". iAlways. iApply lft_incl_trans; first done.
+        iApply lft_intersect_incl_r.
       + iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.
         iFrame "#∗".
       + iIntros (y) "IN". iDestruct "IN" as %->%elem_of_list_singleton.
@@ -300,9 +302,10 @@ Section typing.
     lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗
     qκs.[lft_intersect_list κs] -∗
     (fn fp).(ty_own) tid [f] -∗
-    ([∗ list] y ∈ zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)), tctx_elt_interp tid y) -∗
+    ([∗ list] y ∈ zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)),
+                   tctx_elt_interp tid y) -∗
     (∀ ret, na_own tid top -∗ qκs.[lft_intersect_list κs] -∗
-             (box (fp x).(fp_ty)).(ty_own) tid [ret] -∗ 
+             (box (fp x).(fp_ty)).(ty_own) tid [ret] -∗
              WP k [of_val ret] {{ _, cont_postcondition }}) -∗
     WP (call: f ps → k) {{ _, cont_postcondition }}.
   Proof.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 29dc16690c682f7abb3b7c77b091ef6df6a1bbe7..3cf52a41af1e07000c1aac5c4c1104685f1e2d51 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -151,6 +151,36 @@ Section lft_contexts.
     κ ⊑ₑ κ' ∈ E → lctx_lft_incl κ' κ'' → lctx_lft_incl κ κ''.
   Proof. intros. etrans; last done. by eapply lctx_lft_incl_external. Qed.
 
+  Lemma lctx_lft_incl_intersect κ κ' κ'' :
+    lctx_lft_incl κ κ' → lctx_lft_incl κ κ'' →
+    lctx_lft_incl κ (κ' ⊓ κ'').
+  Proof.
+    iIntros (Hκ' Hκ'' ?) "HL".
+    iDestruct (Hκ' with "HL") as "#Hκ'".
+    iDestruct (Hκ'' with "HL") as "#Hκ''".
+    iIntros "!# #HE". iApply lft_incl_glb. by iApply "Hκ'". by iApply "Hκ''".
+  Qed.
+
+  Lemma lctx_lft_incl_intersect_l κ κ' κ'' :
+    lctx_lft_incl κ κ' →
+    lctx_lft_incl (κ ⊓ κ'') κ'.
+  Proof.
+    iIntros (Hκ' ?) "HL".
+    iDestruct (Hκ' with "HL") as "#Hκ'".
+    iIntros "!# #HE". iApply lft_incl_trans.
+      by iApply lft_intersect_incl_l. by iApply "Hκ'".
+  Qed.
+
+  Lemma lctx_lft_incl_intersect_r κ κ' κ'' :
+    lctx_lft_incl κ κ' →
+    lctx_lft_incl (κ'' ⊓ κ) κ'.
+  Proof.
+    iIntros (Hκ' ?) "HL".
+    iDestruct (Hκ' with "HL") as "#Hκ'".
+    iIntros "!# #HE". iApply lft_incl_trans.
+      by iApply lft_intersect_incl_r. by iApply "Hκ'".
+  Qed.
+
   (* Lifetime aliveness *)
 
   Definition lctx_lft_alive (κ : lft) : Prop :=
@@ -286,26 +316,14 @@ Lemma elctx_sat_submseteq `{invG Σ, lftG Σ} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
 Proof. iIntros (HE' ?) "_ !# H". by iApply big_sepL_submseteq. Qed.
 
-(* TODO: This is not really the right file for stuff like this. *)
-Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
-Hint Resolve of_val_unlock : lrust_typing.
 Hint Resolve
      lctx_lft_incl_relf lctx_lft_incl_static lctx_lft_incl_local'
-     lctx_lft_incl_external'
+     lctx_lft_incl_external' lctx_lft_incl_intersect
+     lctx_lft_incl_intersect_l lctx_lft_incl_intersect_r
      lctx_lft_alive_static lctx_lft_alive_local lctx_lft_alive_external
      elctx_sat_nil elctx_sat_lft_incl elctx_sat_app elctx_sat_refl
-     submseteq_cons submseteq_inserts_l submseteq_inserts_r
   : lrust_typing.
 
 Hint Resolve elctx_sat_submseteq | 100 : lrust_typing.
 
-Hint Extern 1 (@eq nat _ (Z.to_nat _)) => (etrans; [symmetry; exact: Nat2Z.id | reflexivity]) : lrust_typing.
-Hint Extern 1 (@eq nat (Z.to_nat _) _) => (etrans; [exact: Nat2Z.id | reflexivity]) : lrust_typing.
-
-(* FIXME : I would prefer using a [Hint Resolve <-] for this, but
-   unfortunately, this is not preserved across modules. See:
-     https://coq.inria.fr/bugs/show_bug.cgi?id=5189
-   This should be fixed in the next version of Coq. *)
-Hint Extern 1 (_ ∈ _ ++ _) => apply <- @elem_of_app : lrust_typing.
-
 Hint Opaque elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 8722a3fd1cdf11a7aa4af280af5ef134a08ca4d9..45ccd39525e1086f145148a5f1a277c31306ac77 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -991,7 +991,6 @@ Section arc.
          "rcbox" +â‚— #1 <- #1;;
          "rcbox" +â‚— #2 <-{ty.(ty_size)} !"c";;
          delete [ #ty.(ty_size); "c"];;
-         let: "arc''" := !"arc'" in
          "arc'" <- "rcbox";;
          letalloc: "rcold" <- "arc''" in
          (* FIXME : here, we are dropping the old arc pointer. In the
@@ -1069,57 +1068,32 @@ Section arc.
       iApply type_jump; solve_typing.
     - iIntros "[Htok Hν]". wp_case. wp_apply wp_new=>//.
       iIntros (l [|?[]]) "/= (% & H† & Hl)"; try lia. wp_let. wp_op.
-      rewrite heap_mapsto_vec_singleton. wp_write. wp_let. wp_bind (of_val clone).
+      rewrite heap_mapsto_vec_singleton. wp_write. wp_let.
+      wp_bind (of_val clone).
       iApply (wp_wand with "[Hna]").
-      { iApply (Hclone _ [] with "LFT HE Hna");
-        rewrite /llctx_interp /tctx_interp //. }
-      clear Hclone clone. iIntros (clone) "(Hna & _ & [Hclone _])".
-      rewrite tctx_hasty_val. simpl.
-      iDestruct "Hclone" as (fb kb xb ecl ?) "(Heq & % & Hclone)".
-      iDestruct "Heq" as %[=->]. destruct xb as [|?[]]=>//. wp_rec.
-      iMod (lft_create with "LFT") as (β) "[Hβ #Hβ†]"=>//.
-      iMod (bor_create _ β with "LFT Hα2") as "[Hαβ Hα2]"=>//.
-      iMod (bor_fracture (λ q', (q / 2 * q').[α])%I with "LFT [Hαβ]") as "Hαβ'"=>//.
-      { by rewrite Qp_mult_1_r. }
-      iDestruct (frac_bor_lft_incl with "LFT Hαβ'") as "#Hαβ". iClear "Hαβ'".
+      { iApply (Hclone _ [] with "LFT HE Hna"); rewrite /llctx_interp /tctx_interp //. }
+      clear Hclone clone. iIntros (clone) "(Hna & _ & [Hclone _])". rewrite tctx_hasty_val.
       iDestruct "Hs" as "[Hs|Hν']"; last by iDestruct (lft_tok_dead with "Hν Hν'") as "[]".
-      iMod (bor_create _ β with "LFT Hν") as "[Hνβ Hν]"=>//.
-      iMod (bor_fracture (λ q, (q' * q).[ν])%I with "LFT [Hνβ]") as "Hνβ'"=>//.
-      { by rewrite Qp_mult_1_r. }
-      iDestruct (frac_bor_lft_incl with "LFT Hνβ'") as "#Hνβ". iClear "Hνβ'".
-      erewrite <-!(of_to_val (λ: ["_r"], _)%E); [|solve_to_val..].
-      set (K := LamV ["_r"]%RustB _).
-      iApply ("Hclone" $! β β K [# #l] tid with "LFT [] Hna [Hβ] [-H† Hl]")=>/=;
-             last 1 first.
-      { rewrite /tctx_interp big_sepL_singleton tctx_hasty_val' //. simpl.
-        rewrite /= freeable_sz_full. iFrame. iExists [_].
-        rewrite heap_mapsto_vec_singleton /=. iFrame.
-        iApply (ty_shr_mono with "Hνβ Hs"). }
-      { refine ((λ HE : elctx_sat ((β ⊑ₑ α)::_) [] _, _) _).
-        iApply (HE 1%Qp with "[] [$Hαβ $HE]"); by rewrite /llctx_interp. solve_typing. }
-      { rewrite /llctx_interp big_sepL_singleton. iExists β. iFrame "∗#".
-        rewrite left_id //. }
-      rewrite /K /=. clear K. iIntros (?). rewrite elem_of_list_singleton.
-      iIntros "%". subst. iIntros (cl) "Hna Hβ Hcl". inv_vec cl=>cl. simpl. wp_let.
-      rewrite [llctx_interp [β ⊑ₗ []] 1]/llctx_interp big_sepL_singleton.
-      iDestruct "Hβ" as (β') "(Hβeq & Hβ & Hβend)". rewrite /= left_id.
-      iDestruct "Hβeq" as %<-. wp_bind Skip. iSpecialize ("Hβend" with "Hβ").
-      iApply wp_mask_mono; last iApply (wp_step_fupd with "Hβend"); [solve_ndisj..|].
-      wp_seq. iIntros "#Hβ !>". wp_seq. wp_rec.
-      iMod ("Hα2" with "Hβ") as "Hα2". iMod ("Hν" with "Hβ") as "Hν".
-      wp_apply wp_new=>//. iIntros (l' vl) "(% & Hl'† & Hl')". wp_let. wp_op.
-      rewrite shift_loc_0. destruct vl as [|?[|??]]; simpl in *; try lia.
+      iDestruct (lft_intersect_acc with "Hα2 Hν") as (q'') "[Hαν Hclose3]".
+      rewrite -[α ⊓ ν](right_id_L).
+      iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) _ _ _ [_] with
+              "LFT HE Hna Hαν Hclone [Hl H†]"); [solve_typing|solve_to_val| |].
+      { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
+        iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+        iApply ty_shr_mono; last done. iApply lft_intersect_incl_r. }
+      iIntros ([[|cl|]|]) "Hna Hαν Hcl //". wp_rec.
+      iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
+      iDestruct (ty_size_eq with "Hown") as "#%".
+      iDestruct ("Hclose3" with "Hαν") as "[Hα2 Hν]".
+      wp_apply wp_new=>//. iIntros (l' vl') "(% & Hl'† & Hl')". wp_let. wp_op.
+      rewrite shift_loc_0. destruct vl' as [|?[|??]]; simpl in *; try lia.
       rewrite !heap_mapsto_vec_cons shift_loc_assoc.
       iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
-      rewrite tctx_interp_singleton tctx_hasty_val.
-      destruct cl as [[|cl|]|]; try by iDestruct "Hcl" as "[]".
-      iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[>Hcl↦ Hown]".
-      iDestruct (ty_size_eq with "Hown") as "#>%".
       wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]"); [lia..|]. iIntros "[Hl'2 Hcl↦]".
       wp_seq. rewrite freeable_sz_full.
       wp_apply (wp_delete with "[$Hcl↦ Hcl†]");
         [lia|by replace (length vl) with (ty.(ty_size))|].
-      iIntros "_". wp_seq. wp_read. wp_let. wp_write.
+      iIntros "_". wp_seq. wp_write.
       iMod ("Hclose2" $! (shift_loc l' 2 ↦∗: ty_own ty tid)%I with
           "[Hrc'↦ Hl' Hl'1  Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
       { iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 5594c87835522b1579d71df5d1b04bceedbf4a52..1cf22bc9cdf42edb9e38de4e7d1c46c8bf84db81 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -926,7 +926,6 @@ Section code.
       let: "r" := new [ #1 ] in
     withcont: "k":
       let: "rc'" := !"rc" in
-      Newlft;;
       let: "rc''" := !"rc'" in
       let: "strong" := !("rc''" +â‚— #0) in
       if: "strong" = #1 then
@@ -959,17 +958,15 @@ Section code.
         "x" <- "rc''" +â‚— #2;;
         let: "clone" := clone in
         letcall: "c" := "clone" ["x"]%E in (* FIXME : why do I need %E here ? *)
-        Endlft;;
         (* Inlined rc_new("c") begins. *)
         let: "rcbox" := new [ #(2 + ty.(ty_size))%nat ] in
         "rcbox" +â‚— #0 <- #1;;
         "rcbox" +â‚— #1 <- #1;;
         "rcbox" +â‚— #2 <-{ty.(ty_size)} !"c";;
         delete [ #ty.(ty_size); "c"];;
-        let: "rc''" := !"rc'" in
-        letalloc: "rcold" <- "rc''" in
-          (* Inlined rc_new ends. *)
         "rc'" <- "rcbox";;
+        (* Inlined rc_new ends. *)
+        letalloc: "rcold" <- "rc''" in
         (* FIXME : here, we are dropping the old rc pointer. In the
            case another strong reference has been dropped while
            cloning, it is possible that we are actually dropping the
@@ -984,7 +981,8 @@ Section code.
       delete [ #1; "rc"];; return: ["r"].
 
   Lemma rc_make_mut_type ty `{!TyWf ty} clone :
-    typed_val clone (fn(∀ α, ∅; &shr{α} ty) → ty) → (* ty : Clone, as witnessed by the impl clone *)
+    (* ty : Clone, as witnessed by the impl clone *)
+    typed_val clone (fn(∀ α, ∅; &shr{α} ty) → ty) →
     typed_val (rc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α} rc ty) → &uniq{α} ty).
   Proof.
     intros Hclone E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
@@ -998,39 +996,34 @@ Section code.
       iApply type_jump; solve_typing. }
     iIntros (k). simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
-    iApply (type_newlft [α]). iIntros (β).
-    iApply (typed_body_mono _ _ _ _ (reflexivity _)
-            [rc' ◁ &uniq{β} rc ty; rcx ◁ own_ptr 1 (uninit 1);
-             rc' ◁{β} &uniq{α} rc ty; r ◁ own_ptr 1 (uninit 1)]);
-      [simpl; solve_typing|done|].
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hrc' [Hrcx [Hrc'h [Hr _]]]]".
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [Hrc' [Hr _]]]".
     rewrite !tctx_hasty_val [[rcx]]lock [[r]]lock.
     destruct rc' as [[|rc'|]|]; try done.
-    iMod (lctx_lft_alive_tok β with "HE HL") as (q) "(Hβ & HL & Hclose1)"; [solve_typing..|].
-    iMod (bor_acc_cons with "LFT Hrc' Hβ") as "[Hrc' Hclose2]"; first solve_ndisj.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (q) "([Hα1 Hα2] & HL & Hclose1)";
+      [solve_typing..|].
+    iMod (bor_acc_cons with "LFT Hrc' Hα1") as "[Hrc' Hclose2]"; first solve_ndisj.
     iDestruct (heap_mapsto_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
     inv_vec vl=>l. rewrite heap_mapsto_vec_singleton.
     wp_read. destruct l as [[|l|]|]; try done. wp_let. wp_op. rewrite shift_loc_0.
     wp_apply (rc_check_unique with "[$Hna Hrcown]"); first done.
     { (* Boy this is silly... *) iDestruct "Hrcown" as "[(?&?&?&?)|?]"; last by iRight.
       iLeft. by iFrame. }
-    iIntros (c) "(Hl1 & Hc)". wp_let. wp_op; intros Hc.
-    - wp_if. iDestruct "Hc" as "[[% [Hc _]]|[% _]]"; last lia. subst.
+    iIntros (c) "(Hl1 & Hc)". wp_let. wp_op; intros Hc; wp_if.
+    - iDestruct "Hc" as "[[% [Hc _]]|[% _]]"; last lia. subst.
       iDestruct "Hc" as (weak) "[Hl2 Hweak]". wp_op. wp_read. wp_let.
       iDestruct "Hweak" as "[[% Hrc]|[% [_ Hrc]]]".
       + subst. wp_bind (#1 = #1)%E. iApply (wp_step_fupd with "Hrc"); [done..|].
         wp_op=>[_|//]. iIntros "(Hl† & Hty & Hna)!>". wp_if.
-        iMod ("Hclose2" with "[Hrc' Hl1 Hl2 Hl†] [Hty]") as "[Hty Hβ]"; [|iNext; iExact "Hty"|].
+        iMod ("Hclose2" with "[Hrc' Hl1 Hl2 Hl†] [Hty]") as "[Hty Hα1]"; [|iNext; iExact "Hty"|].
         { iIntros "!> Hty". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
           iLeft. by iFrame. }
-        iMod ("Hclose1" with "Hβ HL") as "HL".
-        iApply (type_type _ _ _ [ r ◁ box (uninit 1); #l +ₗ #2 ◁ &uniq{β} ty;
+        iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+        iApply (type_type _ _ _ [ r ◁ box (uninit 1); #l +ₗ #2 ◁ &uniq{α} ty;
                                   rcx ◁ box (uninit 1)]
                 with "[] LFT HE Hna HL Hk [-]"); last first.
-        { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-          unlock. iFrame. }
+        { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
+                  tctx_hasty_val' //. unlock. iFrame. }
         iApply type_assign; [solve_typing..|].
-        iApply type_equivalize_lft.
         iApply type_jump; solve_typing.
       + wp_op; [lia|move=>_]. wp_if. wp_op. rewrite shift_loc_0. wp_write. wp_op.
         wp_op. wp_write. wp_bind (new _). iSpecialize ("Hrc" with "Hl1 Hl2").
@@ -1043,86 +1036,78 @@ Section code.
         wp_apply (wp_memcpy with "[$Hlr3 $H↦vlr]"); [lia..|]. iIntros "[Hlr3 Hvlr]".
         wp_seq. wp_write. wp_op. iMod ("Hproto" with "[Hvlr]") as "Hna"; first by eauto.
         iMod ("Hclose2" $! (shift_loc lr 2 ↦∗: ty_own ty tid)%I
-              with "[Hrc' Hlr1 Hlr2 H†] [Hlr3 Hty]") as "[Hb Hβ]".
+              with "[Hrc' Hlr1 Hlr2 H†] [Hlr3 Hty]") as "[Hb Hα1]".
         { iIntros "!> H !>". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
           iLeft. iFrame. rewrite Z2Nat.inj_pos Pos2Nat.inj_succ SuccNat2Pos.id_succ //. }
         { iExists _. iFrame. }
-        iMod ("Hclose1" with "Hβ HL") as "HL".
-        iApply (type_type _ _ _ [ r ◁ box (uninit 1); #(shift_loc lr 2) ◁ &uniq{β} ty;
+        iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+        iApply (type_type _ _ _ [ r ◁ box (uninit 1); #(shift_loc lr 2) ◁ &uniq{α} ty;
                                   rcx ◁ box (uninit 1)]
                 with "[] LFT HE Hna HL Hk [-]"); last first.
         { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                   tctx_hasty_val' //. unlock. iFrame. }
         iApply type_assign; [solve_typing..|].
-        iApply type_equivalize_lft.
         iApply type_jump; solve_typing.
-    - wp_if. wp_apply wp_new; first lia.
+    - wp_apply wp_new; first lia.
       iIntros (lr [|? [|??]]) "/= (% & [H†|%] & H↦lr)"; try lia.
       iDestruct "Hc" as "[[% ?]|[% [Hproto _]]]"; first lia.
-      iMod ("Hproto" with "Hl1") as "[Hna Hty]".
-      iAssert (ty.(ty_shr) β tid (shift_loc l 2) ∗ (q).[β])%I
-         with "[>Hty Hclose2 Hrc']" as "[Hshr Hβ]".
-      { iDestruct "Hty" as "[(Hl1 & Hl2 & Hl† & Hl3)|Hty]".
-        - iMod ("Hclose2" $! (shift_loc l 2 ↦∗: ty.(ty_own) tid)%I
-            with "[Hrc' Hl1 Hl2 Hl†] Hl3") as "[Hty Hβ]"; first auto.
-          { iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton /=.
-            iFrame. simpl. auto with iFrame. }
-          by iApply (ty_share with "LFT Hty Hβ").
-        - iDestruct "Hty" as (γ ν q') "(Hpersist & Hown & Hν)".
-          iDestruct "Hpersist" as (ty') "(Hty' & ? & #[?|Hν†] & ?)";
-            last by iDestruct (lft_tok_dead with "Hν Hν†") as "[]".
-          iMod ("Hclose2" $! ((q').[ν])%I with "[- Hν] [$Hν]") as "[Hβν $]".
-          { iIntros "!> Hν !>". iExists [_]. rewrite heap_mapsto_vec_singleton.
-            iFrame. iRight. iExists _, _, _. iFrame. auto with iFrame. }
-          iApply (ty_shr_mono with "[>-] [//]").
-          iApply (frac_bor_lft_incl with "LFT").
-          iApply (bor_fracture with "LFT"); first done. by rewrite Qp_mult_1_r. }
-      iMod ("Hclose1" with "Hβ HL") as "HL".
-      rewrite heap_mapsto_vec_singleton. wp_let. wp_op. wp_write.
-      iApply (type_type _ _ _ [ r ◁ box (uninit 1); #lr ◁ box (&shr{β} ty);
-                                #rc' ◁{β} &uniq{α} rc ty; rcx ◁ box (uninit 1)]
-              with "[] LFT HE Hna HL Hk [-]"); last first.
-      { rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
-                  tctx_hasty_val' //. unlock. iFrame.
-        rewrite /= freeable_sz_full_S. iFrame. iExists [_].
-        rewrite heap_mapsto_vec_singleton /=. auto with iFrame. }
-      iApply type_let; [apply Hclone|solve_typing|]. iIntros (clonev). simpl_subst.
-      iApply type_letcall; [solve_typing..|]. iIntros (cl). simpl_subst.
-      iApply type_endlft.
-      clear tid q. iIntros (tid) "_ _ Hna HL Hk [Hcl [_ [Hr [Hrc' [Hrcx _]]]]]".
-      rewrite !tctx_hasty_val [[r]]lock [[rcx]]lock ownptr_own tctx_hasty_val' //.
-      iDestruct "Hcl" as (lcl vlcl) "(% & Hlcl & Hvlcl & Hclfree)". subst.
-      iDestruct (ty_size_eq with "Hvlcl") as "#>Heq".
-      iDestruct "Heq" as %Htysize. wp_apply wp_new; first lia.
-      iIntros (lrc [|?[|? vl]]) "/= (% & [H†|%] & Hlrc)"; try lia.
-      wp_let. wp_op. rewrite shift_loc_0 2!heap_mapsto_vec_cons shift_loc_assoc.
-      iDestruct "Hlrc" as "(Hlrc1 & Hlrc2 & Hlrc3)". wp_write. wp_op. wp_write.
-      wp_op. wp_apply (wp_memcpy with "[$Hlrc3 $Hlcl]"); [lia..|].
-      iIntros "[Hlrc3 Hlcl]". wp_seq. rewrite freeable_sz_full.
-      wp_apply (wp_delete with "[$Hlcl Hclfree]"); [lia|by rewrite Htysize|].
-      iIntros "_". wp_seq.
-      iMod (lctx_lft_alive_tok α with "HE HL")
-        as (q) "(Hα & HL & Hclose1)"; [solve_typing..|].
-      iMod (bor_acc_cons with "LFT Hrc' Hα") as "[Hrc' Hclose2]"; first solve_ndisj.
-      iDestruct "Hrc'" as ([| [[|rcold|]|] [|]]) "[Hrc' Hty]";
-        try by iDestruct "Hty" as ">[]".
-      rewrite heap_mapsto_vec_singleton [[ #rcold]]lock. wp_read. wp_let.
-      wp_apply wp_new; first done. iIntros (lrcold [|?[]]) "/= (% & [?|%] & ?)"; try lia.
-      wp_let. rewrite heap_mapsto_vec_singleton. wp_write. wp_write.
-      iMod ("Hclose2" $! (shift_loc lrc 2 ↦∗: ty.(ty_own) tid)%I
-            with "[Hlrc1 Hlrc2 Hrc' H†] [Hlrc3 Hvlcl]") as "[Hb Hα]".
-      { iIntros "!> H". iExists [ #lrc]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
-        rewrite Z2Nat.inj_pos Pos2Nat.inj_succ SuccNat2Pos.id_succ /=. auto with iFrame. }
-      { iExists _. iFrame. }
-      iMod ("Hclose1" with "Hα HL") as "HL".
-      iApply (type_type _ _ _ [ r ◁ box (uninit 1); #lrc +ₗ #2 ◁ &uniq{α} ty;
-                                rcx ◁ box (uninit 1); #lrcold ◁ box (rc ty) ]
+      iMod ("Hproto" with "Hl1") as "[Hna Hty]". wp_let. wp_op.
+      rewrite heap_mapsto_vec_singleton. wp_write.
+      iAssert (∃ γ ν q, rc_persist tid ν γ l ty ∗ own γ (rc_tok q) ∗ q.[ν])%I
+        with "[>Hty]" as (γ ν q') "(Hty & Htok & Hν)".
+      { iDestruct "Hty" as "[(Hl1 & Hl2 & Hl† & Hl3)|Hty]"; last done.
+        iMod (own_alloc (● (Some $ Cinl ((1/2)%Qp, 1%positive), 0%nat) ⋅
+                         rc_tok (1/2)%Qp)) as (γ) "[Ha Hf]"=>//.
+        iMod (lft_create with "LFT") as (ν) "[[Hν1 Hν2] Hν†]"=>//.
+        iApply (fupd_mask_mono (↑lftN))=>//. iExists γ, ν, (1/2)%Qp. iFrame.
+        iMod (bor_create _ ν with "LFT Hl3") as "[Hb Hh]"=>//. iExists _.
+        iSplitR; first by iApply type_incl_refl.
+        iMod (ty_share with "LFT Hb Hν1") as "[Hty Hν]"=>//.
+        iSplitR "Hty"; last by auto. iApply na_inv_alloc. iExists _. do 2 iFrame.
+        iExists _. iFrame. by rewrite Qp_div_2. }
+      iDestruct "Hty" as (ty') "#(Hty'ty & Hinv & Hs & Hν†)".
+      iDestruct "Hs" as "[Hs|Hν']"; last by iDestruct (lft_tok_dead with "Hν Hν'") as "[]".
+      wp_bind (of_val clone). iApply (wp_wand with "[Hna]").
+      { iApply (Hclone _ [] with "LFT HE Hna").
+          by rewrite /llctx_interp. by rewrite /tctx_interp. }
+      clear clone Hclone. iIntros (clone) "(Hna & _ & Hclone)".
+      wp_let. wp_let. rewrite tctx_interp_singleton tctx_hasty_val.
+      iDestruct (lft_intersect_acc with "Hα2 Hν") as (q'') "[Hαν Hclose3]".
+      rewrite -[α ⊓ ν](right_id_L).
+      iApply (type_call_iris _ [α ⊓ ν] (α ⊓ ν) _ _ _ [_]
+              with "LFT HE Hna Hαν Hclone [H† H↦lr]"); [solve_typing|solve_to_val| |].
+      { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full_S.
+        iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+        iApply ty_shr_mono; last done. iApply lft_intersect_incl_r. }
+      iIntros ([[|cl|]|]) "Hna Hαν Hcl //". wp_rec.
+      iDestruct "Hcl" as "[Hcl Hcl†]". iDestruct "Hcl" as (vl) "[Hcl↦ Hown]".
+      iDestruct (ty_size_eq with "Hown") as "#%".
+      iDestruct ("Hclose3" with "Hαν") as "[Hα2 Hν]".
+      wp_apply wp_new=>//. iIntros (l' vl') "(% & Hl'† & Hl')". wp_let. wp_op.
+      rewrite shift_loc_0. destruct vl' as [|?[|??]]; simpl in *; try lia.
+      rewrite !heap_mapsto_vec_cons shift_loc_assoc.
+      iDestruct "Hl'" as "(Hl' & Hl'1 & Hl'2)". wp_write. wp_op. wp_write. wp_op.
+      wp_apply (wp_memcpy with "[$Hl'2 $Hcl↦]"); [lia..|]. iIntros "[Hl'2 Hcl↦]".
+      wp_seq. rewrite freeable_sz_full.
+      wp_apply (wp_delete with "[$Hcl↦ Hcl†]");
+        [lia|by replace (length vl) with (ty.(ty_size))|].
+      iIntros "_". wp_seq. wp_write.
+      iMod ("Hclose2" $! (shift_loc l' 2 ↦∗: ty_own ty tid)%I with
+          "[Hrc' Hl' Hl'1  Hl'†] [Hl'2 Hown]") as "[Hl' Hα1]".
+      { iIntros "!> H". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame.
+        iLeft. iFrame. iDestruct "Hl'†" as "[?|%]"=>//.
+        by rewrite /Z.to_nat Pos2Nat.inj_succ SuccNat2Pos.id_succ. }
+      { iExists _.  iFrame. }
+      iMod ("Hclose1" with "[$Hα1 $Hα2] HL") as "HL".
+      iApply (type_type _ _ _ [ #l ◁ rc ty; #l' +ₗ #2 ◁ &uniq{α} ty;
+                                r ◁ box (uninit 1); rcx ◁ box (uninit 1) ]
               with "[] LFT HE Hna HL Hk [-]"); last first.
       { rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
-                !tctx_hasty_val' //. rewrite /= freeable_sz_full_S.
-        unlock. iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. }
-      iApply type_let; [apply rc_drop_type|solve_typing|]. iIntros (drop). simpl_subst.
-      iApply (type_letcall ()); [try solve_typing..|].
+                !tctx_hasty_val' //. unlock. iFrame. iRight. iExists γ, ν, _.
+        iFrame "∗#". auto. }
+      iApply type_letalloc_1; [solve_typing..|]. iIntros (rcold). simpl_subst.
+      iApply type_let. apply rc_drop_type. solve_typing. iIntros (drop). simpl_subst.
+      iApply (type_letcall ()); try solve_typing.
       { (* FIXME : solve_typing should be able to do this. *)
         move=>ϝ' /=. change (ty_outlives_E (option ty) ϝ') with (ty_outlives_E ty ϝ').
         solve_typing. }
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 6e07357b4b736ecd85f9bdaf57bb103cebc330b3..0b84223455dce1c9b862e7854833583689091802 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -207,23 +207,22 @@ Section ref_functions.
   Definition ref_map (call_once : val) : val :=
     funrec: <> ["ref"; "f"] :=
       let: "call_once" := call_once in
-      Newlft;;
       let: "x'" := !"ref" in
       letalloc: "x" <- "x'" in
       letcall: "r" := "call_once" ["f"; "x"]%E in
       let: "r'" := !"r" in delete [ #1; "r"];;
-      Endlft;;
       "ref" <- "r'";;
       return: ["ref"].
 
   Lemma ref_map_type ty1 ty2 call_once fty `{!TyWf ty1, !TyWf ty2, !TyWf fty} :
-    typed_val call_once (fn(∀ α, ∅; fty, &shr{α}ty1) → &shr{α}ty2) → (* fty : for<'a>, FnOnce(&'a ty1) -> &'a ty2, as witnessed by the impl call_once *)
+    (* fty : for<'a>, FnOnce(&'a ty1) -> &'a ty2, as witnessed by the impl call_once *)
+    typed_val call_once (fn(∀ α, ∅; fty, &shr{α}ty1) → &shr{α}ty2) →
     typed_val (ref_map call_once) (fn(∀ α, ∅; ref α ty1, fty) → ref α ty2).
   Proof.
     intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
        inv_vec arg=>ref env. simpl_subst.
     iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
-    iApply (type_newlft [ϝ]). iIntros (κ tid) "#LFT #HE Hna HL Hk (#Hf' & Href & Henv & _)".
+    iIntros (tid) "#LFT #HE Hna HL Hk (#Hf' & Href & Henv & _)".
     rewrite (tctx_hasty_val _ ref). destruct ref as [[|lref|]|]; try done.
     iDestruct "Href" as "[Href Href†]".
     iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
@@ -233,45 +232,32 @@ Section ref_functions.
     iDestruct "Href" as (ν qν γ β ty') "(#Hshr & #Hαβ & #Hinv & >Hν & Hγ)".
     wp_read. wp_let. wp_apply wp_new; first done.
     iIntros (lx [|? []]) "(% & H† & Hlx)"; try (simpl in *; lia).
-    rewrite heap_mapsto_vec_singleton. wp_let. wp_write.
-    match goal with | |- context [(WP (_ [?k']) {{_, _}})%I] =>
-      assert (∃ k, to_val k' = Some k) as [k EQk] by (eexists; solve_to_val) end.
-    iApply (wp_let' _ _ _ _ k _ EQk). simpl_subst. iNext.
-    iDestruct (lctx_lft_incl_incl κ α with "HL HE") as "#Hκα"; [solve_typing..|].
-    iMod (bor_create _ κ (qν).[ν] with "LFT [$Hν]") as "[Hb Hν]"; first done.
-    iAssert (κ ⊑ α ⊓ ν)%I with "[>Hb]" as "#Hκν".
-    { iApply (lft_incl_glb with "Hκα"). iApply (frac_bor_lft_incl with "LFT").
-      iApply (bor_fracture with "LFT [> -]"); first done. rewrite /= Qp_mult_1_r //. }
-    iApply (type_type ((κ ⊑ₑ α ⊓ ν) :: (α ⊓ ν ⊑ₑ α) :: _) _
-        [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box (&shr{α ⊓ ν}ty2)])]
-        [ f' ◁ fn(∀ α, ∅; fty, &shr{α}ty1) → &shr{α}ty2;
-          #lx ◁ box (&shr{α ⊓ ν}ty1); env ◁ box fty ]
-       with "[] LFT [] Hna HL [-H† Hlx Henv]"); swap 1 2; swap 3 4.
-    { iSplitL; last iSplitL; [done|iApply lft_intersect_incl_l|iApply "HE"]. }
-    { iApply (type_call (α ⊓ ν)); solve_typing. }
-    { rewrite /tctx_interp /=. iFrame "Hf' Henv".
-      iApply tctx_hasty_val'; first done. rewrite -freeable_sz_full.
-      iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. auto. }
-    iIntros (? ->%elem_of_list_singleton arg) "Hna HL Hr". inv_vec arg=>r.
-    apply of_to_val in EQk. rewrite EQk. iApply wp_rec; try (done || apply _).
-    { repeat econstructor. by rewrite to_of_val. } simpl_subst.
-    rewrite /tctx_interp big_sepL_singleton (tctx_hasty_val _ r) ownptr_own.
-    iDestruct "Hr" as (lr vr) "(% & Hlr & Hvr & H†)". subst. inv_vec vr=>r'. iNext.
+    rewrite heap_mapsto_vec_singleton. wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
+    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
+    iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
+    iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
+    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L).
+    iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) _ _ _ [_; _]
+       with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H†]"); [solve_typing|solve_to_val|done| |].
+    { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
+      iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
+    iIntros ([[|r|]|]) "Hna Hανϝ Hr //".
+    iDestruct ("Hclose4" with "Hανϝ") as "[Hαν Hϝ]".
+    iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
+    iMod ("Hclose2" with "Hϝ HL") as "HL". iMod ("Hclose1" with "Hα HL") as "HL".
+    wp_rec. iDestruct "Hr" as "[Hr Hr†]".
+    iDestruct "Hr" as ([|r'[]]) "[Hr #Hr']";
+      try by iDestruct (ty_size_eq with "Hr'") as "%".
     rewrite heap_mapsto_vec_singleton. wp_read. wp_let.
-    wp_apply (wp_delete _ _ _ [_] with "[Hlr H†]"). done.
-    { rewrite heap_mapsto_vec_singleton freeable_sz_full. iFrame. }
-    iIntros "_". wp_seq. wp_bind Endlft. iDestruct "HL" as "[Hκ HL]".
-    iDestruct "Hκ" as (κ') "(% & Hκ' & #Hκ'†)". simpl in *. subst κ.
-    iSpecialize ("Hκ'†" with "Hκ'").
-    iApply wp_mask_mono; last iApply (wp_step_fupd with "Hκ'†"); auto with ndisj.
-    wp_seq. iIntros "Hκ'† !>". iMod ("Hν" with "[Hκ'†]") as "Hν";
-      first by rewrite -lft_dead_or; auto. wp_seq. wp_write.
+    wp_apply (wp_delete _ _ _ [_] with "[Hr Hr†]")=>//.
+    { rewrite heap_mapsto_vec_singleton freeable_sz_full. iFrame. } iIntros "_".
+    wp_seq. wp_write.
     iApply (type_type _ [_] _ [ #lref ◁ box (ref α ty2) ]
-       with "[] LFT HE Hna [HL] Hk"); first last.
-    { rewrite tctx_interp_singleton. iExists _. iSplit. done.
-      iFrame. iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+       with "[] LFT HE Hna HL Hk"); first last.
+    { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame.
+      iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
       iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
-    { rewrite /llctx_interp /=; auto. }
     iApply type_jump; solve_typing.
   Qed.
 End ref_functions.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 2dc9b2e57b11e065eb870ccf8c1638007a8bb59a..020157d6e73a459dc6affee8d6c08bf69e353bee 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -154,23 +154,22 @@ Section refmut_functions.
   Definition refmut_map (call_once : val) : val :=
     funrec: <> ["ref"; "f"] :=
       let: "call_once" := call_once in
-      Newlft;;
       let: "x'" := !"ref" in
       letalloc: "x" <- "x'" in
       letcall: "r" := "call_once" ["f"; "x"]%E in
       let: "r'" := !"r" in delete [ #1; "r"];;
-      Endlft;;
       "ref" <- "r'";;
       return: ["ref"].
 
   Lemma refmut_map_type ty1 ty2 call_once fty `{!TyWf ty1, !TyWf ty2, !TyWf fty} :
-    typed_val call_once (fn(∀ α, ∅; fty, &uniq{α}ty1) → &uniq{α}ty2) → (* fty : for<'a>, FnOnce(&'a ty1) -> &'a ty2, as witnessed by the impl call_once *)
+    (* fty : for<'a>, FnOnce(&'a ty1) -> &'a ty2, as witnessed by the impl call_once *)
+    typed_val call_once (fn(∀ α, ∅; fty, &uniq{α}ty1) → &uniq{α}ty2) →
     typed_val (refmut_map call_once) (fn(∀ α, ∅; refmut α ty1, fty) → refmut α ty2).
   Proof.
     intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
        inv_vec arg=>ref env. simpl_subst.
     iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
-    iApply (type_newlft [ϝ]). iIntros (κ tid) "#LFT #HE Hna HL Hk (#Hf' & Href & Henv & _)".
+    iIntros (tid) "#LFT #HE Hna HL Hk (#Hf' & Href & Henv & _)".
     rewrite (tctx_hasty_val _ ref). destruct ref as [[|lref|]|]; try done.
     iDestruct "Href" as "[Href Href†]".
     iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
@@ -180,45 +179,33 @@ Section refmut_functions.
     iDestruct "Href" as (ν γ β ty') "(Hbor & #Hαβ & #Hinv & >Hν & Hγ)".
     wp_read. wp_let. wp_apply wp_new; first done.
     iIntros (lx [|? []]) "(% & H† & Hlx)"; try (simpl in *; lia).
-    rewrite heap_mapsto_vec_singleton. wp_let. wp_write.
-    match goal with | |- context [(WP (_ [?k']) {{_, _}})%I] =>
-      assert (∃ k, to_val k' = Some k) as [k EQk] by (eexists; solve_to_val) end.
-    iApply (wp_let' _ _ _ _ k _ EQk). simpl_subst. iNext.
-    iDestruct (lctx_lft_incl_incl κ α with "HL HE") as "#Hκα"; [solve_typing..|].
-    iMod (bor_create _ κ (1).[ν] with "LFT [$Hν]") as "[Hb Hν]"; first done.
-    iAssert (κ ⊑ α ⊓ ν)%I with "[>Hb]" as "#Hκν".
-    { iApply (lft_incl_glb with "Hκα"). iApply (frac_bor_lft_incl with "LFT").
-      iApply (bor_fracture with "LFT [> -]"); first done. rewrite /= Qp_mult_1_r //. }
-    iApply (type_type ((κ ⊑ₑ α ⊓ ν) :: (α ⊓ ν ⊑ₑ α) :: _) _
-        [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box (&uniq{α ⊓ ν}ty2)])]
-        [ f' ◁ fn(∀ α, ∅; fty, &uniq{α}ty1) → &uniq{α}ty2;
-          #lx ◁ box (&uniq{α ⊓ ν}ty1); env ◁ box fty ]
-       with "[] LFT [] Hna HL [-H† Hlx Henv Hbor]"); swap 1 2; swap 3 4.
-    { iSplitL; last iSplitL; [done|iApply lft_intersect_incl_l|iApply "HE"]. }
-    { iApply (type_call (α ⊓ ν)); solve_typing. }
-    { rewrite /tctx_interp /=. iFrame "Hf' Henv".
-      iApply tctx_hasty_val'; first done. rewrite -freeable_sz_full.
-      iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. auto with iFrame. }
-    iIntros (? ->%elem_of_list_singleton arg) "Hna HL Hr". inv_vec arg=>r.
-    apply of_to_val in EQk. rewrite EQk. iApply wp_rec; try (done || apply _).
-    { repeat econstructor. by rewrite to_of_val. } simpl_subst.
-    rewrite /tctx_interp big_sepL_singleton (tctx_hasty_val _ r) ownptr_own.
-    iDestruct "Hr" as (lr vr) "(% & Hlr & Hvr & H†)". subst. inv_vec vr=>r'. iNext.
+    rewrite heap_mapsto_vec_singleton. wp_let. wp_write. wp_let. rewrite tctx_hasty_val.
+    iMod (lctx_lft_alive_tok α with "HE HL") as (?) "(Hα & HL & Hclose1)";[solve_typing..|].
+    iMod (lctx_lft_alive_tok ϝ with "HE HL") as (?) "(Hϝ & HL & Hclose2)";[solve_typing..|].
+    iDestruct (lft_intersect_acc with "Hα Hν") as (?) "[Hαν Hclose3]".
+    iDestruct (lft_intersect_acc with "Hαν Hϝ") as (?) "[Hανϝ Hclose4]".
+    rewrite -[ϝ in (α ⊓ ν) ⊓ ϝ](right_id_L).
+    iApply (type_call_iris _ [α ⊓ ν; ϝ] (α ⊓ ν) _ _ _ [_; _]
+            with "LFT HE Hna [Hανϝ] Hf' [$Henv Hlx H† Hbor]");
+      [solve_typing|solve_to_val|done| |].
+    { rewrite big_sepL_singleton tctx_hasty_val' //. rewrite /= freeable_sz_full.
+      iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame. }
+    iIntros ([[|r|]|]) "Hna Hανϝ Hr //".
+    iDestruct ("Hclose4" with "Hανϝ") as "[Hαν Hϝ]".
+    iDestruct ("Hclose3" with "Hαν") as "[Hα Hν]".
+    iMod ("Hclose2" with "Hϝ HL") as "HL". iMod ("Hclose1" with "Hα HL") as "HL".
+    wp_rec. iDestruct "Hr" as "[Hr Hr†]".
+    iDestruct "Hr" as ([|r'[]]) "[Hr Hr']";
+      try by iDestruct (ty_size_eq with "Hr'") as "%".
     rewrite heap_mapsto_vec_singleton. wp_read. wp_let.
-    wp_apply (wp_delete _ _ _ [_] with "[Hlr H†]"). done.
-    { rewrite heap_mapsto_vec_singleton freeable_sz_full. iFrame. }
-    iIntros "_". wp_seq. wp_bind Endlft. iDestruct "HL" as "[Hκ HL]".
-    iDestruct "Hκ" as (κ') "(% & Hκ' & #Hκ'†)". simpl in *. subst κ.
-    iSpecialize ("Hκ'†" with "Hκ'").
-    iApply wp_mask_mono; last iApply (wp_step_fupd with "Hκ'†"); auto with ndisj.
-    wp_seq. iIntros "Hκ'† !>". iMod ("Hν" with "[Hκ'†]") as "Hν";
-      first by rewrite -lft_dead_or; auto. wp_seq. wp_write.
+    wp_apply (wp_delete _ _ _ [_] with "[Hr Hr†]")=>//.
+    { rewrite heap_mapsto_vec_singleton freeable_sz_full. iFrame. } iIntros "_".
+    wp_seq. wp_write.
     iApply (type_type _ [_] _ [ #lref ◁ box (refmut α ty2) ]
-       with "[] LFT HE Hna [HL] Hk"); first last.
-    { rewrite tctx_interp_singleton tctx_hasty_val. iExists _. iSplit. done.
-      iFrame. iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
+       with "[] LFT HE Hna HL Hk"); first last.
+    { rewrite tctx_interp_singleton tctx_hasty_val' //. iFrame.
+      iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
       iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
-    { rewrite /llctx_interp /=; auto. }
     iApply type_jump; solve_typing.
   Qed.
 End refmut_functions.