diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index e0927db166a62743512b439e5923f5898e7d4469..b2bf7ce811f697d4038fc602338087cb393b3dcd 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -163,9 +163,9 @@ Proof.
                 -fmap_None -lookup_fmap !fmap_delete //. }
     rewrite own_bor_op. iDestruct "Hbor" as "[H● H◯]".
     iAssert (&{κ}(P ∗ Q))%I with "[H◯ Hslice]" as "$".
-    { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ∪ κ2). 
+    { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ∪ κ2).
       iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2").
-      iExists γ. iFrame. } 
+      iExists γ. iFrame. }
     iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
     iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
     rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index 9d933ae479c00a59beb7978708c066e882b21ca1..73b28d1018be895950c35c637f3180878493133d 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -58,7 +58,17 @@ Proof.
   - iMod "Hclose". by iApply (bor_fake with "LFT").
 Qed.
 
-Lemma bor_persistent P `{!PersistentP P} E κ q :
+Lemma bor_persistent P `{!PersistentP P} E κ :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ}P ={E}=∗ ▷ P ∨ [†κ].
+Proof.
+  iIntros (?) "#LFT Hb".
+  iMod (bor_acc_atomic with "LFT Hb") as "[[#HP Hob]|[#H† Hclose]]"; first done.
+  - iMod ("Hob" with "HP") as "_". auto.
+  - iMod "Hclose" as "_". auto.
+Qed.
+
+Lemma bor_persistent_tok P `{!PersistentP P} E κ q :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
 Proof.
@@ -67,7 +77,6 @@ Proof.
   by iMod ("Hob" with "HP") as "[_ $]".
 Qed.
 
-
 Lemma lft_incl_static κ : (κ ⊑ static)%I.
 Proof.
   iIntros "!#". iSplitR.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 0ae322ab26367de69ec9e9fd703cb7ab126d01ce..d8de200fc9c3a36bb5e32ad378100c321fa5f28d 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -111,7 +111,14 @@ Section frac_bor.
     iApply (lft_incl_trans with "Hκκ' []"). auto.
   Qed.
 
-  Lemma frac_bor_incl κ κ' q:
+  Lemma frac_bor_fake E κ Φ:
+    ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &frac{κ}Φ.
+  Proof.
+    iIntros (?) "#LFT#H†". iApply (bor_fracture with "LFT >"). done.
+    by iApply (bor_fake with "LFT").
+  Qed.
+
+  Lemma frac_bor_lft_incl κ κ' q:
     lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
   Proof.
     iIntros "#LFT#Hbor!#". iSplitR.
@@ -123,7 +130,6 @@ Section frac_bor.
       iDestruct "H" as (q') "[>Hκ' _]".
       iDestruct (lft_tok_dead with "Hκ' H†'") as "[]".
   Qed.
-
 End frac_bor.
 
 Typeclasses Opaque frac_bor.
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index 4f5042ef4c7e63c05d7cb32aea0fd79835dd8461..f31b4a095f5d55ece99ed4c3c7b9d7322421c7c2 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/theories/lifetime/shr_borrow.v
@@ -51,6 +51,11 @@ Section shared_bors.
       by iApply (idx_bor_shorten with "H⊑").
   Qed.
 
+  Lemma shr_bor_fake E κ: ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &shr{κ}P.
+  Proof.
+    iIntros (?) "#LFT#H†". iApply (bor_share with ">"). done.
+    by iApply (bor_fake with "LFT H†").
+  Qed.
 End shared_bors.
 
 Typeclasses Opaque shr_bor.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index a23272ff51ff0d195bc5fd425cf35261914cfe19..c04fe440a3685559273417caf996570b6a89b221 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -16,7 +16,7 @@ Section fn.
   Next Obligation.
     iIntros (n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
   Qed.
-  Next Obligation. intros. by iIntros "_ _ $". Qed.
+  Next Obligation. intros. by iIntros "_ _". Qed.
   Next Obligation. intros. by iIntros "_ _ _". Qed.
 
   (* TODO : For now, functions are not Send. This means they cannot be
@@ -49,10 +49,11 @@ Section fn.
     - iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
       iIntros (x vl) "!#[Hρ2 Htl]". iApply ("Hwp" with ">").
       iFrame. iApply (Hρ1ρ2 with "LFT"). by iFrame.
-    - iSplit; last done. simpl. iDestruct "H" as (vl0) "[? Hvl]".
-      iExists vl0. iFrame "#". iNext. iDestruct "Hvl" as (f) "[% Hwp]".
-      iExists f. iSplit. done. iIntros (x vl) "!#[Hρ2 Htl]".
-      iApply ("Hwp" with ">"). iFrame. iApply (Hρ1ρ2 with "LFT >"). by iFrame.
+    - iSplit; last done. simpl. iDestruct "H" as (vl0) "[? [Hvl|H†]]".
+      + iExists vl0. iFrame "#". iLeft. iNext. iDestruct "Hvl" as (f) "[% Hwp]".
+        iExists f. iSplit. done. iIntros (x vl) "!#[Hρ2 Htl]".
+        iApply ("Hwp" with ">"). iFrame. iApply (Hρ1ρ2 with "LFT >"). by iFrame.
+      + iExists _. iFrame "#". by iRight.
   Qed.
 
   Lemma ty_incl_fn_cont {A n} ρ ρf (x : A) :
@@ -70,9 +71,11 @@ Section fn.
     - iDestruct "H" as (fv) "[%#H]". subst. iExists _. iSplit. done.
       iIntros (x vl). by iApply "H".
     - iSplit; last done.
-      iDestruct "H" as (fvl) "[?Hown]". iExists _. iFrame. iNext.
-      iDestruct "Hown" as (fv) "[%H]". subst. iExists _. iSplit. done.
-      iIntros (x vl). by iApply "H".
+      iDestruct "H" as (fvl) "[?[Hown|H†]]".
+      + iExists _. iFrame. iLeft. iNext.
+        iDestruct "Hown" as (fv) "[%H]". subst. iExists _. iSplit. done.
+        iIntros (x vl). by iApply "H".
+      + iExists _. iFrame. by iRight.
   Qed.
 
   Lemma typed_fn {A n} `{Duplicable _ ρ, Closed (f :b: xl +b+ []) e} θ :
@@ -117,5 +120,4 @@ Section fn.
     iDestruct ("IH" with "Hρ") as (f') "[Hf' IH']".
     iDestruct "Hf'" as %[=<-]. iApply ("IH'" with "Hθ Htl").
   Qed.
-
 End fn.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index c0d98404057ee77d00b456dbc45cf3d53f324677..983739b3b3b6199d02c9ba4d45130a13804a8bef 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -58,45 +58,45 @@ Section own.
                    â–· freeable_sz n ty.(ty_size) l)%I;
        ty_shr κ tid E l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
-            □ (∀ q' F, ⌜E ∪ mgmtE ⊆ F⌝ →
-                 q'.[κ] ={F,F∖E}▷=∗ ty.(ty_shr) κ tid E l' ∗ q'.[κ]))%I
+            □ (∀ F, ⌜E ∪ mgmtE ⊆ F⌝ ={F,F∖E∖↑lftN}▷=∗ ty.(ty_shr) κ tid E l' ∨ [†κ]))%I
     |}.
   Next Obligation.
     iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
   Next Obligation.
-    move=> q ty E N κ l tid q' ?? /=. iIntros "#LFT Hshr Htok".
+    move=>n ty E N κ l tid ?? /=. iIntros "#LFT Hshr".
     iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
     iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
+    iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver. iExists l'.
     iMod (bor_sep with "LFT Hb2") as "[EQ Hb2]". set_solver.
-    iMod (bor_persistent with "LFT EQ Htok") as "[>% $]". set_solver. subst.
-    rewrite heap_mapsto_vec_singleton.
-    iMod (bor_sep with "LFT Hb2") as "[Hb2 _]". set_solver.
-    iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
-    rewrite bor_unfold_idx. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
-    iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty κ tid (↑N) l')%I
-         with "[Hpbown]") as "#Hinv"; first by eauto.
-    iExists l'. iIntros "!>{$Hbf}!#". iIntros (q'' F) "% Htok".
-    iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
-    iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "H". set_solver.
-      { rewrite bor_unfold_idx. eauto. }
-      iModIntro. iNext. iMod "H" as "[Hb Htok]".
-      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]". done. set_solver.
-      iApply "Hclose". auto.
-    - iModIntro. iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
+    iMod (bor_persistent with "LFT EQ") as "[>%|#H†]". set_solver.
+    - subst. rewrite heap_mapsto_vec_singleton.
+      iMod (bor_sep with "LFT Hb2") as "[Hb2 _]". set_solver.
+      iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
+      rewrite bor_unfold_idx. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
+      iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty κ tid (↑N) l')%I
+            with "[Hpbown]") as "#Hinv"; first by eauto.
+      iIntros "!>!#*%". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
+      iDestruct "INV" as "[>Hbtok|#Hshr]".
+      + iMod (bor_later with "LFT [Hbtok]") as "Hb". set_solver.
+        { rewrite bor_unfold_idx. eauto. }
+        iModIntro. iNext. iMod "Hb". iLeft.
+        iMod (ty.(ty_share) with "LFT Hb") as "#$". done. set_solver.
+        iApply "Hclose". auto.
+      + iMod fupd_intro_mask' as "Hclose'"; last iModIntro. set_solver.
+        iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
+    - iSplitL. by iApply (frac_bor_fake with "LFT"). iIntros "!>!#*_".
+      iApply step_fupd_intro. set_solver. auto.
   Qed.
   Next Obligation.
     intros _ ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
     iDestruct "H" as (l') "[Hfb #Hvs]".
-    iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!#".
-    iIntros (q' F) "% Htok".
-    iApply (step_fupd_mask_mono F _ _ (F∖E)). set_solver. set_solver.
-    iMod (lft_incl_acc with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
-    iMod ("Hvs" with "* [%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
-    iMod "Hvs'" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
-      by iApply (ty.(ty_shr_mono) with "LFT Hκ").
+    iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros "!#*%".
+    iApply (step_fupd_mask_mono F _ _ (F∖E∖↑lftN)). set_solver. set_solver.
+    iMod ("Hvs" with "* [%]") as "Hvs'". set_solver. iModIntro. iNext.
+    iMod "Hvs'" as "[Hshr|H†]".
+    - iLeft. by iApply (ty.(ty_shr_mono) with "LFT Hκ").
+    - iRight. iApply (lft_incl_dead with "Hκ H†"). set_solver.
   Qed.
 
   Global Instance own_mono E L n :
@@ -115,9 +115,10 @@ Section own.
     - iIntros (qE qL) "#LFT HE HL *".
       iDestruct (Hincl.(subtype_shr _ _ _ _) with "LFT HE HL") as "#Hshri".
       iIntros "{HE HL} !# * H". iDestruct "H" as (l') "[Hfb #Hvs]".
-      iExists l'. iFrame. iIntros "!#". iIntros (q' F') "% Hκ".
-      iMod ("Hvs" with "* [%] Hκ") as "Hvs'". done. iModIntro. iNext.
-      iMod "Hvs'" as "[Hshr $]". iApply ("Hshri" with "* Hshr").
+      iExists l'. iFrame. iIntros "!#". iIntros (F') "%".
+      iMod ("Hvs" with "* [%]") as "Hvs'". done. iModIntro. iNext.
+      iMod "Hvs'" as "[Hshr|H†]"; last by auto.
+      iLeft. iApply ("Hshri" with "* Hshr").
   Qed.
 
   Global Instance own_proper E L n :
diff --git a/theories/typing/perm.v b/theories/typing/perm.v
index e7f1520023d3dff470264abc5dc1ed2c2fdb25c9..39206bead992d2d52659fa4b44a6845953c9fc80 100644
--- a/theories/typing/perm.v
+++ b/theories/typing/perm.v
@@ -215,7 +215,7 @@ Section perm_incl.
     iMod (bor_create with "LFT [$Htok]") as "[Hbor Hclose]". done.
     iMod (bor_fracture (λ q', (q * q').[κ'])%I with "LFT [Hbor]") as "Hbor". done.
     { by rewrite Qp_mult_1_r. }
-    iSplitL "Hbor". iApply (frac_bor_incl with "LFT Hbor").
+    iSplitL "Hbor". iApply (frac_bor_lft_incl with "LFT Hbor").
     iIntros "!>H". by iMod ("Hclose" with "H") as ">$".
   Qed.
 End perm_incl.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 5acd25fb2d3d97c887c97d2d874474e495bf7d41..df7fde178f0079129e9a3357d44e6bff326d0e48 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -40,11 +40,10 @@ Section product.
     iDestruct "H1" as %->. iDestruct "H2" as %->. done.
   Qed.
   Next Obligation.
-    intros ty1 ty2 E N κ l tid q ??. iIntros "#LFT /=H Htok".
-    rewrite split_prod_mt.
+    intros ty1 ty2 E N κ l tid ??. iIntros "#LFT /=H". rewrite split_prod_mt.
     iMod (bor_sep with "LFT H") as "[H1 H2]". set_solver.
-    iMod (ty1.(ty_share) _ (N .@ 1) with "LFT H1 Htok") as "[? Htok]". solve_ndisj. done.
-    iMod (ty2.(ty_share) _ (N .@ 2) with "LFT H2 Htok") as "[? $]". solve_ndisj. done.
+    iMod (ty1.(ty_share) _ (N .@ 1) with "LFT H1") as "?". solve_ndisj. done.
+    iMod (ty2.(ty_share) _ (N .@ 2) with "LFT H2") as "?". solve_ndisj. done.
     iModIntro. iExists (↑N .@ 1). iExists (↑N .@ 2). iFrame.
     iPureIntro. split. solve_ndisj. split; apply nclose_subseteq.
   Qed.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 13e15a5d11d52ce25139830cb941d70614f3f789..4ec050d8781d91b31266d12f988ad187a71e6a32 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -1,3 +1,4 @@
+From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import frac_borrow.
 From lrust.typing Require Export type.
@@ -14,7 +15,7 @@ Section shr_bor.
     iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
 
-  Global Instance subtype_shr_mono E L :
+  Global Instance subtype_shr_bor_mono E L :
     Proper (flip (incl E L) ==> subtype E L ==> subtype E L) shr_bor.
   Proof.
     intros κ1 κ2 Hκ ty1 ty2 Hty. split.
@@ -25,17 +26,18 @@ Section shr_bor.
       iSplit. done. by iApply (ty2.(ty_shr_mono) with "LFT Hκ"); last iApply "Hty".
     - iIntros (qE qL) "#LFT HE HL *". iDestruct (Hκ with "HE HL") as "#Hκ".
       iDestruct (subtype_shr _ _ _ _ Hty with "LFT HE HL") as "#Hst".
-      iIntros "{HE HL}!#*H". iDestruct "H" as (vl) "#[Hfrac Hty]".
-      iExists vl. iFrame "#". iNext.
-      iDestruct "Hty" as (l0) "(% & Hty)". subst. iExists _. iSplit. done.
-      by iApply (ty_shr_mono with "LFT Hκ"); last iApply "Hst".
+      iIntros "{HE HL}!#*H". iDestruct "H" as (vl) "#[Hfrac [Hty|H†]]".
+      + iExists vl. iFrame "#". iLeft. iNext. simpl.
+        iDestruct "Hty" as (l0) "(% & Hty)". subst. iExists _. iSplit. done.
+          by iApply (ty_shr_mono with "LFT Hκ"); last iApply "Hst".
+      + simpl. eauto.
   Qed.
-  Global Instance subtype_shr_mono' E L :
+  Global Instance subtype_shr_bor_mono' E L :
     Proper (incl E L ==> flip (subtype E L) ==> flip (subtype E L)) shr_bor.
-  Proof. intros ??????. by apply subtype_shr_mono. Qed.
-  Global Instance subtype_shr_proper E L κ :
+  Proof. intros ??????. by apply subtype_shr_bor_mono. Qed.
+  Global Instance subtype_shr_bor_proper E L κ :
     Proper (eqtype E L ==> eqtype E L) (shr_bor κ).
-  Proof. intros ??[]. by split; apply subtype_shr_mono. Qed.
+  Proof. intros ??[]. by split; apply subtype_shr_bor_mono. Qed.
 End shr_bor.
 
 Notation "&shr{ κ } ty" := (shr_bor κ ty)
@@ -44,14 +46,14 @@ Notation "&shr{ κ } ty" := (shr_bor κ ty)
 Section typing.
   Context `{typeG Σ}.
 
-  Lemma perm_incl_share q ν κ ty :
-    ν ◁ &uniq{κ} ty ∗ q.[κ] ⇒ ν ◁ &shr{κ} ty ∗ q.[κ].
+  Lemma tctx_incl_share E L p κ ty :
+    tctx_incl E L [TCtx_holds p (&uniq{κ}ty)] [TCtx_holds p (&shr{κ}ty)].
   Proof.
-    iIntros (tid) "#LFT [Huniq [Htok $]]". unfold has_type.
-    destruct (eval_expr ν); last by iDestruct "Huniq" as "[]".
+    iIntros (??) "#LFT _ _ !# * Huniq". rewrite /tctx_interp !big_sepL_singleton /=.
+    iDestruct "Huniq" as (v) "[% Huniq]". iExists _. iFrame "%".
     iDestruct "Huniq" as (l P) "[[% #HPiff] HP]".
     iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
-    iMod (ty.(ty_share) _ lrustN with "LFT H↦ Htok") as "[Hown $]"; [solve_ndisj|done|].
+    iMod (ty.(ty_share) _ lrustN with "LFT H↦") as "Hown"; [solve_ndisj|done|].
     iIntros "!>/=". eauto.
   Qed.
 
@@ -93,14 +95,16 @@ Section typing.
     iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑ & Htok) & $)". wp_bind ν.
     iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
-    iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
+    iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
     iDestruct "H↦" as (vl) "[H↦b #Hown]".
-    iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
-    iApply (wp_fupd_step _ (⊤∖↑lrustN) with "[Hown Htok2]"); try done.
-    - iApply ("Hown" with "* [%] Htok2"). set_solver.
-    - wp_read. iIntros "!>[Hshr ?]". iFrame "H⊑".
-      iSplitL "Hshr"; first by iExists _; auto. iApply ("Hclose" with ">").
-      iFrame. iApply "Hclose'". auto.
+    iMod (frac_bor_acc with "LFT H↦b Htok") as (q''') "[>H↦ Hclose']". done.
+    iApply (wp_fupd_step _ (⊤∖↑lrustN∖↑lftN) with "[Hown]"); try done.
+    - iApply ("Hown" with "* [%]"). set_solver.
+    - wp_read. iIntros "!>[Hshr|#H†]{$H⊑}".
+      + iSplitL "Hshr"; first by iExists _; auto. iApply ("Hclose" with ">").
+        iFrame. iApply "Hclose'". auto.
+      + iMod ("Hclose'" with "[H↦]"). by auto.
+        by iDestruct (lft_tok_dead with "[-] H†") as "[]".
   Qed.
 
   Lemma typed_deref_shr_bor_bor ty ν κ κ' κ'' q:
@@ -112,16 +116,17 @@ Section typing.
     iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq Hshr]".
     iDestruct "Heq" as %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
-    iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
-    iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
+    iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[Htok Hclose]". done.
+    iMod (frac_bor_acc with "LFT H↦ Htok") as (q'') "[>H↦ Hclose']". done.
     iAssert (κ' ⊑ κ'' ∪ κ')%I as "#H⊑3".
     { iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
-    iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
-    iApply (wp_fupd_step _ (_∖_) with "[Hown Htok]"); try done.
-    - iApply ("Hown" with "* [%] Htok"). set_solver.
-    - wp_read. iIntros "!>[Hshr Htok]". iFrame "H⊑1". iSplitL "Hshr".
-      + iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
-      + iApply ("Hclose" with ">"). iMod ("Hclose'" with "[$H↦]") as "$".
-        by iMod ("Hclose''" with "Htok") as "$".
+    iApply (wp_fupd_step _ (_∖_) with "[Hown]"); try done.
+    - iApply ("Hown" with "* [%]"). set_solver.
+    - wp_read. iIntros "!>[#Hshr|#H†]{$H⊑1}".
+      + iSplitR.
+        * iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
+        * iApply ("Hclose" with ">"). iApply ("Hclose'" with "[$H↦]").
+      + iMod ("Hclose'" with "[H↦]"). by auto.
+        by iDestruct (lft_tok_dead with "[-] H†") as "[]".
   Qed.
 End typing.
\ No newline at end of file
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 4bfb93ffbdbd5164b3bce169421ae66ccb5af122..82c649be712d59b17ac7d541e4f3ad8f7ed1e15b 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -6,24 +6,10 @@ From lrust.typing Require Import type_incl.
 Section sum.
   Context `{typeG Σ}.
 
-  (* [emp] cannot be defined using [ty_of_st], because the least we
-     would be able to prove from its [ty_shr] would be [â–· False], but
-     we really need [False] to prove [ty_incl_emp]. *)
-  Program Definition emp :=
-    {| ty_size := 0; ty_own tid vl := False%I; ty_shr κ tid E l := False%I |}.
+  Program Definition emp : type := {| st_size := 0; st_own tid vl := False%I |}.
   Next Obligation. iIntros (tid vl) "[]". Qed.
-  Next Obligation.
-    iIntros (????????) "#LFT Hb Htok".
-    iMod (bor_exists with "LFT Hb") as (vl) "Hb". set_solver.
-    iMod (bor_sep with "LFT Hb") as "[_ Hb]". set_solver.
-    iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]". set_solver.
-  Qed.
-  Next Obligation. intros. iIntros "_ _ []". Qed.
   Global Instance emp_empty : Empty type := emp.
 
-  Global Program Instance emp_copy : Copy emp.
-  Next Obligation. intros. iIntros "_ []". Qed.
-
   Lemma split_sum_mt l tid q tyl :
     (l ↦∗{q}: λ vl,
          ∃ (i : nat) vl', ⌜vl = #i :: vl'⌝ ∗ ty_own (nth i tyl ∅) tid vl')%I
@@ -66,10 +52,10 @@ Section sum.
     subst. simpl. by iDestruct (sum_size_eq with "Hown") as %->.
   Qed.
   Next Obligation.
-    intros n tyl Hn E N κ l tid q ??. iIntros "#LFT Hown Htok". rewrite split_sum_mt.
+    intros n tyl Hn E N κ l tid ??. iIntros "#LFT Hown". rewrite split_sum_mt.
     iMod (bor_exists with "LFT Hown") as (i) "Hown". set_solver.
     iMod (bor_sep with "LFT Hown") as "[Hmt Hown]". set_solver.
-    iMod ((nth i tyl ∅).(ty_share) with "LFT Hown Htok") as "[#Hshr $]"; try done.
+    iMod ((nth i tyl ∅).(ty_share) with "LFT Hown") as "#Hshr"; try done.
     iMod (bor_fracture with "LFT [-]") as "H"; last by eauto. set_solver. iFrame.
   Qed.
   Next Obligation.
@@ -109,7 +95,6 @@ Section sum.
       rewrite heap_mapsto_vec_prop_op; last (by intros; apply sum_size_eq, Hn).
       by iApply "Hclose'".
   Qed.
-
 End sum.
 
 Existing Instance LstTySize_nil.
@@ -125,8 +110,10 @@ Notation "Σ[ ty1 ; .. ; tyn ]" :=
 Section incl.
   Context `{typeG Σ}.
 
+   (* FIXME : do we need that anywhere?. *)
   Lemma ty_incl_emp ρ ty : ty_incl ρ ∅ ty.
-  Proof. iIntros (tid) "_ _!>". iSplit; iIntros "!#*/=[]". Qed.
+  Proof.
+  Admitted.
 
   Lemma ty_incl_sum ρ n tyl1 tyl2 (_ : LstTySize n tyl1) (_ : LstTySize n tyl2) :
     Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 →
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 4d212d8c97a4ae8855ac748dcb2509e30c16a233..39ca984e10e0d904592706e594bff00dfd9bd91e 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -35,8 +35,8 @@ Section type.
          invariants, which does not need the mask.  Moreover, it is
          more consistent with thread-local tokens, which we do not
          give any. *)
-      ty_share E N κ l tid q : mgmtE ⊥ ↑N → mgmtE ⊆ E →
-        lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗ ty_shr κ tid (↑N) l ∗ q.[κ];
+      ty_share E N κ l tid : mgmtE ⊥ ↑N → mgmtE ⊆ E →
+        lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) ={E}=∗ ty_shr κ tid (↑N) l;
       ty_shr_mono κ κ' tid E E' l : E ⊆ E' →
         lft_ctx -∗ κ' ⊑ κ -∗ ty_shr κ tid E l -∗ ty_shr κ' tid E' l
     }.
@@ -71,37 +71,43 @@ Section type.
           borrow, otherwise I do not know how to prove the shr part of
           [subtype_shr_mono]. *)
        ty_shr := λ κ tid _ l,
-                 (∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗ ▷ st.(st_own) tid vl)%I
+                 (∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗
+                        (▷ st.(st_own) tid vl ∨ □|={↑lftN}=>[†κ]))%I
     |}.
   Next Obligation. intros. apply st_size_eq. Qed.
   Next Obligation.
-    intros st E N κ l tid q ? ?. iIntros "#LFT Hmt Htok".
+    intros st E N κ l tid ? ?. iIntros "#LFT Hmt".
     iMod (bor_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
     iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]". set_solver.
-    iMod (bor_persistent with "LFT Hown Htok") as "[Hown $]". set_solver.
-    iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; last first.
-    { iExists vl. by iFrame. }
-    done. set_solver.
+    iMod (bor_persistent with "LFT Hown") as "[Hown|#H†]". set_solver.
+    - iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; last first.
+      { iExists vl. iFrame. auto. }
+      done. set_solver.
+    - iExists []. iSplitL; last by auto. iApply (frac_bor_fake with "LFT"); auto.
   Qed.
   Next Obligation.
     intros st κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
-    iDestruct "H" as (vl) "[Hf Hown]".
-    iExists vl. iFrame. by iApply (frac_bor_shorten with "Hord").
+    iDestruct "H" as (vl) "[#Hf #Hown]".
+    iExists vl. iSplit. by iApply (frac_bor_shorten with "Hord").
+    iDestruct "Hown" as "[Hown|#H†]". auto. iRight. iIntros "!#".
+    by iApply (lft_incl_dead with "Hord >").
   Qed.
 
   Global Program Instance ty_of_st_copy st : Copy (ty_of_st st).
   Next Obligation.
     intros st κ tid E F l q ?. iIntros "#LFT #Hshr[Hlft $]".
-    iDestruct "Hshr" as (vl) "[Hf Hown]".
-    iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
-    iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
-    - iNext. iExists _. by iFrame.
-    - iIntros "Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
-      iAssert (▷ ⌜length vl = length vl'⌝)%I as ">%".
-      { iNext. iDestruct (st_size_eq with "Hown") as %->.
-        iDestruct (st_size_eq with "Hown'") as %->. done. }
-      iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
-      iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
+    iDestruct "Hshr" as (vl) "[Hf [Hown|#H†]]".
+    - iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
+      iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
+      + iNext. iExists _. by iFrame.
+      + iIntros "Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
+        iAssert (▷ ⌜length vl = length vl'⌝)%I as ">%".
+        { iNext. iDestruct (st_size_eq with "Hown") as %->.
+          iDestruct (st_size_eq with "Hown'") as %->. done. }
+        iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
+        iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
+    - iApply fupd_mask_mono; last iMod "H†". set_solver.
+      iDestruct (lft_tok_dead with "Hlft H†") as "[]".
   Qed.
 End type.
 
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index b23985b01284529b3ffc088e9054ba4abf75f716..7d4bce1fe7bef14d7954534df73b4ada688ea111 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -39,7 +39,7 @@ Section type_context.
 
   Definition tctx_incl (E : lectx) (L : llctx) (T1 T2 : tctx): Prop :=
     ∀ qE qL, lft_ctx -∗ lectx_interp E qE -∗ llctx_interp L qL -∗
-          □ ∀ tid, tctx_interp tid T1 -∗ tctx_interp tid T2.
+          □ ∀ tid, tctx_interp tid T1 ={⊤}=∗ tctx_interp tid T2.
 
   Global Instance tctx_incl_preorder E L : PreOrder (tctx_incl E L).
   Proof.
@@ -48,7 +48,7 @@ Section type_context.
     - iIntros (??? H1 H2 ??) "#LFT HE HL".
       iDestruct (H1 with "LFT HE HL") as "#H1".
       iDestruct (H2 with "LFT HE HL") as "#H2".
-      iIntros "{HE HL}!# * H". iApply "H2". by iApply "H1".
+      iIntros "{HE HL}!# * H". iApply ("H2" with ">"). by iApply "H1".
   Qed.
 
   Lemma contains_tctx_incl E L T1 T2 : T1 `contains` T2 → tctx_incl E L T2 T1.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 94c3f5ee9c72fcd79003c0350d0d4a795cc21f9f..d4971ab93ea7b617eba862ef49a0c1e53be7bc77 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -15,36 +15,37 @@ Section uniq_bor.
          (∃ (l:loc) P, (⌜vl = [ #l ]⌝ ∗ □ (P ↔ l ↦∗: ty.(ty_own) tid)) ∗ &{κ} P)%I;
        ty_shr κ' tid E l :=
          (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
-            □ ∀ q' F, ⌜E ∪ mgmtE ⊆ F⌝ → q'.[κ∪κ']
-               ={F, F∖E∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∗ q'.[κ∪κ'])%I
+            □ ∀ F, ⌜E ∪ mgmtE ⊆ F⌝
+                ={F, F∖E∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∨ [†κ'])%I
     |}.
   Next Obligation.
     iIntros (q ty tid vl) "H". iDestruct "H" as (l P) "[[% _] _]". by subst.
   Qed.
   Next Obligation.
-    move=> κ ty E N κ' l tid q' ??/=. iIntros "#LFT Hshr Htok".
+    move=> κ ty E N κ' l tid ??/=. iIntros "#LFT Hshr".
     iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
     iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
+    iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver. iExists l'.
     iMod (bor_exists with "LFT Hb2") as (P) "Hb2". set_solver.
     iMod (bor_sep with "LFT Hb2") as "[H Hb2]". set_solver.
-    iMod (bor_persistent with "LFT H Htok") as "[[>% #HPiff] $]". set_solver. subst.
-    rewrite heap_mapsto_vec_singleton.
-    iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
-    rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
-    iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid (↑N) l')%I
-         with "[Hpbown]") as "#Hinv"; first by eauto.
-    iExists l'. iIntros "!>{$Hbf}!#". iIntros (q'' F) "% Htok".
-    iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
-    iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_unnest _ _ _ P with "LFT [Hbtok]") as "Hb".
-      { set_solver. } { iApply bor_unfold_idx. eauto. }
-      iModIntro. iNext. iMod "Hb".
-      iMod (bor_iff with "LFT [] Hb") as "Hb". set_solver. by eauto.
-      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; try done. set_solver.
-      iApply "Hclose". eauto.
-    - iMod ("Hclose" with "[]") as "_". by eauto.
-      iApply step_fupd_mask_mono; last by eauto. done. set_solver.
+    iMod (bor_persistent with "LFT H") as "[[>% #HPiff]|#H†]". set_solver.
+    - subst. rewrite heap_mapsto_vec_singleton.
+      iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
+      rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
+      iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid (↑N) l')%I
+            with "[Hpbown]") as "#Hinv"; first by eauto.
+      iIntros "!>!#*%". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
+      iDestruct "INV" as "[>Hbtok|#Hshr]".
+      + iMod (bor_unnest _ _ _ P with "LFT [Hbtok]") as "Hb".
+        { set_solver. } { iApply bor_unfold_idx. eauto. }
+        iModIntro. iNext. iMod "Hb".
+        iMod (bor_iff with "LFT [] Hb") as "Hb". set_solver. by eauto.
+        iMod (ty.(ty_share) with "LFT Hb") as "#Hshr". done. set_solver.
+        iMod ("Hclose" with "[]") as "_"; auto.
+      + iMod ("Hclose" with "[]") as "_". by eauto.
+        iApply step_fupd_intro. set_solver. auto.
+    - iSplitL. by iApply (frac_bor_fake with "LFT"). iIntros "!>!#*_".
+      iApply step_fupd_intro. set_solver. auto.
   Qed.
   Next Obligation.
     intros κ0 ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
@@ -54,12 +55,12 @@ Section uniq_bor.
       - iApply (lft_incl_trans with "[] Hκ").
         iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
     iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
-    iIntros "!#". iIntros (q F) "% Htok".
-    iApply (step_fupd_mask_mono F _ _ (F∖E∖ ↑lftN)). set_solver. set_solver.
-    iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]". set_solver.
-    iMod ("Hvs" with "* [%] Htok") as "Hvs'". set_solver. iModIntro. iNext.
-    iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
-      by iApply (ty_shr_mono with "LFT Hκ0").
+    iIntros "!#*%".
+    iApply (step_fupd_mask_mono F _ _ (F∖E∖ ↑lftN)); try  set_solver.
+    iMod ("Hvs" with "* [%]") as "Hvs'". set_solver. iModIntro. iNext.
+    iMod "Hvs'" as "[#Hshr|H†]".
+    - iLeft. by iApply (ty_shr_mono with "LFT Hκ0").
+    - iRight. iApply (lft_incl_dead with "Hκ H†"). set_solver.
   Qed.
 
   Global Instance subtype_uniq_mono E L :
@@ -84,12 +85,10 @@ Section uniq_bor.
         - iApply (lft_incl_trans with "[] Hκ"). iApply lft_le_incl.
             apply gmultiset_union_subseteq_l.
         - iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
-      iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!#".
-      iIntros (q' F') "% Htok".
-      iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
-      iMod ("Hupd" with "* [%] Htok") as "Hupd'"; try done. iModIntro. iNext.
-      iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
-      iApply (ty_shr_mono with "LFT Hincl'"); last by iApply "Hty". done.
+      iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!#%%".
+      iMod ("Hupd" with "* [%]") as "Hupd'"; try done. iModIntro. iNext.
+      iMod "Hupd'" as "[H|H†]"; last by auto.
+      iLeft. iApply (ty_shr_mono with "LFT Hincl'"); last by iApply "Hty". done.
   Qed.
   Global Instance subtype_uniq_mono' E L :
     Proper (incl E L ==> eqtype E L ==> flip (subtype E L)) uniq_bor.
@@ -194,7 +193,7 @@ Section typing.
     iMod (bor_exists with "LFT Hbor") as (l') "Hbor". done.
     iMod (bor_exists with "LFT Hbor") as (P') "Hbor". done.
     iMod (bor_sep with "LFT Hbor") as "[H Hbor]". done.
-    iMod (bor_persistent with "LFT H Htok") as "[[>% #HP'iff] Htok]". done. subst.
+    iMod (bor_persistent_tok with "LFT H Htok") as "[[>% #HP'iff] Htok]". done. subst.
     iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
     rewrite heap_mapsto_vec_singleton.
     iApply (wp_fupd_step  _ (⊤∖↑lftN) with "[Hbor]"); try done.