diff --git a/theories/lifetime.v b/theories/lifetime.v
index 6bb618a1b73f95f41ee94853cee41c3aa09587e6..a0c79716e2616d95d8536f47c66bb1bae8501073 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -11,11 +11,17 @@ Definition atomic_lft := positive.
 Definition lft_tokUR : ucmraT :=
   authUR (gmapUR atomic_lft (csumR fracR unitR)).
 
+(* FIXME : this is not the actual definitions. *)
+Definition borrow_idx := positive.
+Definition borrow_tokUR : ucmraT :=
+  authUR (gmapUR borrow_idx fracR).
+
 Class lifetimeG Σ := LifetimeG {
-  lifetimeG_inv_inG :> invG Σ;
   lft_tok_inG :> inG Σ lft_tokUR;
+  borrow_tok_inG :> inG Σ borrow_tokUR;
   frac_inG :> inG Σ fracR;
-  toks_name : gname
+  lft_toks_name : gname;
+  borrow_tok_name : gname
 }.
 
 Section defs.
@@ -35,39 +41,36 @@ Section defs.
     end.
 
   Definition lft_own (q : Qp) (κ : lifetime) : iProp Σ :=
-    own toks_name (◯ (Cinl <$> omap (Qp_nat_mul q) κ)).
+    own lft_toks_name (◯ (Cinl <$> omap (Qp_nat_mul q) κ)).
 
   Definition lft_dead (κ : lifetime) : iProp Σ :=
     (∃ Λ, ■ (∃ n, κ !! Λ = Some (S n)) ∗
-            own toks_name (◯ {[ Λ := Cinr () ]}))%I.
+            own lft_toks_name (◯ {[ Λ := Cinr () ]}))%I.
+
+  Definition idx_borrow_own (q : Qp) (i : borrow_idx) :=
+    own borrow_tok_name (â—¯ {[ i := q ]}).
 
 End defs.
 
 Typeclasses Opaque lft_own lft_dead .
 
-Parameter lft_extract :
-  ∀ `{lifetimeG Σ} (κ : lifetime) (P : iProp Σ), iProp Σ.
-Parameter lft_idx_borrow:
-  ∀ `{lifetimeG Σ} (κ : lifetime) (i : gname) (P : iProp Σ), iProp Σ.
-Parameter lft_idx_borrow_persist: ∀ `{lifetimeG Σ} (i : gname), iProp Σ.
-Parameter lft_idx_borrow_own : ∀ `{lifetimeG Σ} (i : gname), iProp Σ.
+Parameter idx_borrow:
+  ∀ `{lifetimeG Σ} (κ : lifetime) (i : borrow_idx) (P : iProp Σ), iProp Σ.
 
-Definition lft_borrow `{lifetimeG Σ} (κ : lifetime) (P : iProp Σ) : iProp Σ :=
-  (∃ i, lft_idx_borrow κ i P ∗ lft_idx_borrow_own i)%I.
+Definition borrow `{lifetimeG Σ} (κ : lifetime) (P : iProp Σ) : iProp Σ :=
+  (∃ i, idx_borrow κ i P ∗ idx_borrow_own 1 i)%I.
 
 (*** Notations  *)
 
 Notation "q .[ κ ]" := (lft_own q κ)
     (format "q .[ κ ]", at level 0): uPred_scope.
 Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
-Notation "κ ∋ P" := (lft_extract κ P)
-  (at level 75, right associativity) : uPred_scope.
-Notation "&{ κ } P" := (lft_borrow κ P)
+Notation "&{ κ } P" := (borrow κ P)
   (format "&{ κ } P", at level 20, right associativity) : uPred_scope.
 Hint Unfold lifetime : typeclass_instances.
 
 Section lft.
-  Context `{lifetimeG Σ}.
+  Context `{invG Σ, lifetimeG Σ}.
 
   (*** PersitentP, TimelessP and Proper instances  *)
 
@@ -79,28 +82,18 @@ Section lft.
   Global Instance lft_dead_timeless κ : PersistentP [†κ].
   Proof. unfold lft_dead. apply _. Qed.
 
-  Axiom lft_idx_borrow_persistent :
-    ∀ κ i P, PersistentP (lft_idx_borrow κ i P).
-  Global Existing Instance lft_idx_borrow_persistent.
-  Axiom lft_idx_borrow_proper :
-    ∀ κ i, Proper ((⊣⊢) ==> (⊣⊢)) (lft_idx_borrow κ i).
-  Global Existing Instance lft_idx_borrow_proper.
-
-  Axiom lft_idx_borrow_persist_persistent :
-    ∀ i, PersistentP (lft_idx_borrow_persist i).
-  Global Existing Instance lft_idx_borrow_persist_persistent.
-  Axiom lft_idx_borrow_persist_timeless :
-    ∀ i, TimelessP (lft_idx_borrow_persist i).
-  Global Existing Instance lft_idx_borrow_persist_timeless.
+  Axiom idx_borrow_persistent :
+    ∀ κ i P, PersistentP (idx_borrow κ i P).
+  Global Existing Instance idx_borrow_persistent.
+  Axiom idx_borrow_proper :
+    ∀ κ i, Proper ((⊣⊢) ==> (⊣⊢)) (idx_borrow κ i).
+  Global Existing Instance idx_borrow_proper.
 
-  Axiom lft_idx_borrow_own_timeless :
-    ∀ i, TimelessP (lft_idx_borrow_own i).
-  Global Existing Instance lft_idx_borrow_own_timeless.
+  Axiom idx_borrow_own_timeless :
+    ∀ q i, TimelessP (idx_borrow_own q i).
+  Global Existing Instance idx_borrow_own_timeless.
 
-  Axiom lft_extract_proper : ∀ κ, Proper ((⊣⊢) ==> (⊣⊢)) (lft_extract κ).
-  Global Existing Instances lft_extract_proper.
-
-  Global Instance lft_borrow_proper κ: Proper ((⊣⊢) ==> (⊣⊢)) (lft_borrow κ).
+  Global Instance borrow_proper κ: Proper ((⊣⊢) ==> (⊣⊢)) (borrow κ).
   Proof. solve_proper. Qed.
 
   (** Basic rules about lifetimes  *)
@@ -136,49 +129,40 @@ Section lft.
     rewrite -!assoc. f_equal. apply (comm _).
   Qed.
 
-  (* FIXME : merging begin and end. *)
   Axiom lft_create :
     ∀ `(nclose lftN ⊆ E), True ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,∅}▷=∗ [†κ]).
 
-  Axiom lft_idx_borrow_persist_upd :
-    ∀ `(nclose lftN ⊆ E) i, lft_idx_borrow_own i ={E}=∗ lft_idx_borrow_persist i.
-  Axiom lft_idx_borrow_own_acc :
+  Axiom idx_borrow_acc :
     ∀ `(nclose lftN ⊆ E) q κ i P,
-      lft_idx_borrow κ i P ⊢ lft_idx_borrow_own i ∗ q.[κ] ={E}=∗ ▷ P ∗
-                                 (▷ P ={E}=∗ lft_idx_borrow_own i ∗ q.[κ]).
-  Axiom lft_idx_borrow_persist_acc :
+      idx_borrow κ i P ⊢ idx_borrow_own 1 i ∗ q.[κ] ={E}=∗ ▷ P ∗
+                                 (▷ P ={E}=∗ idx_borrow_own 1 i ∗ q.[κ]).
+  (* TODO : Can't we give back ▷ P ∨ [†κ] in all cases?  *)
+  Axiom idx_borrow_atomic_acc :
     ∀ `(nclose lftN ⊆ E) q κ i P,
-      lft_idx_borrow κ i P ⊢ lft_idx_borrow_persist i -∗
-            q.[κ] ={E,E∖lftN}=∗ ▷ P ∗ (▷ P ={E∖lftN,E}=∗ q.[κ]).
+      idx_borrow κ i P ⊢ idx_borrow_own q i
+         ={E,E∖lftN}=∗
+            ▷ P ∗ (▷ P ={E∖lftN,E}=∗ idx_borrow_own q i) ∨
+            [†κ] ∗ (|={E∖lftN,E}=> idx_borrow_own q i).
 
   (** Basic borrows  *)
-  Axiom lft_borrow_create :
-    ∀ `(nclose lftN ⊆ E) κ P, ▷ P ={E}=∗ &{κ} P ∗ κ ∋ ▷ P.
-  Axiom lft_borrow_split :
+  Axiom borrow_create :
+    ∀ `(nclose lftN ⊆ E) κ P, ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
+  Axiom borrow_split :
     ∀ `(nclose lftN ⊆ E) κ P Q, &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
-  Axiom lft_borrow_combine :
+  Axiom borrow_combine :
     ∀ `(nclose lftN ⊆ E) κ P Q, &{κ}P ∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
-  Axiom lft_borrow_acc_strong :
+  Axiom borrow_acc_strong :
     ∀ `(nclose lftN ⊆ E) q κ P,
       &{κ}P ⊢ q.[κ] ={E}=∗ ▷ P ∗
-      ∀ Q, ▷ Q ∗ ▷([†κ] ∗ ▷Q  ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
-  Axiom lft_reborrow_static :
+      ∀ Q, ▷ Q ∗ ▷([†κ] ∗ ▷Q ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
+  Axiom borrow_reborrow' :
     ∀ `(nclose lftN ⊆ E) κ κ' P, κ ≼ κ' →
-      &{κ}P ={E}=∗ &{κ'}P ∗ κ' ∋ &{κ}P.
+      &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
   (* FIXME : the document says that we need κ tokens here. Why so?
      Why not κ' tokens also?*)
-  Axiom lft_borrow_unnest :
+  Axiom borrow_unnest :
     ∀ `(nclose lftN ⊆ E) κ κ' P, &{κ'}&{κ}P ⊢ |={E}▷=> &{κ ⋅ κ'}P.
 
-  (** Extraction  *)
-  Axiom lft_extract_split :
-    ∀ `(nclose lftN ⊆ E) κ P Q, κ ∋ (P ∗ Q) ={E}=∗ κ ∋ P ∗ κ ∋ Q.
-  Axiom lft_extract_combine :
-    ∀ `(nclose lftN ⊆ E) κ P Q, κ ∋ P ∗ κ ∋ Q ={E}=∗ κ ∋ (P ∗ Q).
-  Axiom lft_extract_out : ∀ `(nclose lftN ⊆ E) κ P, [†κ] ⊢ κ ∋ P ={E}=∗ P.
-  Axiom lft_extract_contravar : ∀ κ P Q, (P -∗ Q) ∗ κ ∋ P ⊢ κ ∋ Q.
-  Axiom lft_extract_mono : ∀ κ κ' P, κ' ≼ κ → κ ∋ P ⊢ κ' ∋ P.
-
   (*** Derived lemmas  *)
 
   Lemma lft_own_dead q κ : q.[κ] ∗ [† κ] ⊢ False.
@@ -194,7 +178,13 @@ Section lft.
   Lemma lft_own_static q : True ==∗ q.[static].
   Proof.
     rewrite /lft_own /static omap_empty fmap_empty.
-    apply (own_empty (A:=lft_tokUR) toks_name).
+    apply (own_empty (A:=lft_tokUR) lft_toks_name).
+  Qed.
+
+  Lemma lft_not_dead_static : [† static] ⊢ False.
+  Proof.
+    rewrite /lft_dead /static. setoid_rewrite lookup_empty.
+    iIntros "HΛ". iDestruct "HΛ" as (Λ) "[% _]". naive_solver.
   Qed.
 
   Lemma lft_own_split κ q : q.[κ] ⊣⊢ (q/2).[κ] ∗ (q/2).[κ].
@@ -228,116 +218,133 @@ Section lft.
     FromSep q.[κ1⋅κ2] q.[κ1] q.[κ2].
   Proof. by rewrite /FromSep lft_own_op. Qed.
 
-  Lemma lft_borrow_acc E q κ P : nclose lftN ⊆ E →
+  Lemma borrow_acc E q κ P : nclose lftN ⊆ E →
       &{κ}P ⊢ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
   Proof.
     iIntros (?) "HP Htok".
-    iMod (lft_borrow_acc_strong with "HP Htok") as "[HP Hclose]". done.
+    iMod (borrow_acc_strong with "HP Htok") as "[HP Hclose]". done.
     iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP}!>[_$]".
   Qed.
 
-  Lemma lft_borrow_exists {A} `(nclose lftN ⊆ E)
+  Lemma borrow_exists {A} `(nclose lftN ⊆ E)
         κ q (Φ : A → iProp Σ) {_:Inhabited A}:
     &{κ}(∃ x, Φ x) ⊢ q.[κ] ={E}=∗ ∃ x, &{κ}Φ x ∗ q.[κ].
   Proof.
     iIntros "Hb Htok".
-    iMod (lft_borrow_acc_strong with "Hb Htok") as "[HΦ Hob]". done.
+    iMod (borrow_acc_strong with "Hb Htok") as "[HΦ Hob]". done.
     iDestruct "HΦ" as (x) "HΦ". iExists x. iApply "Hob". iIntros "{$HΦ}!>[_?]". eauto.
   Qed.
 
-  Lemma lft_borrow_or `(nclose lftN ⊆ E) κ q P Q:
+  Lemma borrow_or `(nclose lftN ⊆ E) κ q P Q:
     &{κ}(P ∨ Q) ⊢ q.[κ] ={E}=∗ (&{κ}P ∨ &{κ}Q) ∗ q.[κ].
   Proof.
     iIntros "H Htok". rewrite uPred.or_alt.
-    iMod (lft_borrow_exists with "H Htok") as ([]) "[H $]"; auto.
+    iMod (borrow_exists with "H Htok") as ([]) "[H $]"; auto.
   Qed.
 
-  Lemma lft_borrow_persistent `(nclose lftN ⊆ E) `{PersistentP _ P} κ q:
+  Lemma borrow_persistent `(nclose lftN ⊆ E) `{PersistentP _ P} κ q:
     &{κ}P ⊢ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
   Proof.
     iIntros "Hb Htok".
-    iMod (lft_borrow_acc with "Hb Htok") as "[#HP Hob]". done.
+    iMod (borrow_acc with "Hb Htok") as "[#HP Hob]". done.
     by iMod ("Hob" with "HP") as "[_$]".
   Qed.
 
+  (* TODO : is this derivable (problem with masks of inheritance)? *)
+  (* Lemma borrow_unnest' `(nclose lftN ⊆ E) κ κ' q P: *)
+  (*   &{κ'}&{κ}P ⊢ q.[κ'] ={E}▷=∗ q.[κ'] ∗ &{κ ⋅ κ'}P. *)
+  (* Proof. *)
+
 End lft.
 
-Typeclasses Opaque lft_borrow.
+Typeclasses Opaque borrow.
 
 (*** Inclusion and shortening. *)
 
-Definition lft_incl `{lifetimeG Σ} κ κ' : iProp Σ :=
-  (□ ∀ q, q.[κ] ={lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={lftN}=∗ q.[κ]))%I.
+Definition lft_incl `{invG Σ, lifetimeG Σ} κ κ' : iProp Σ :=
+  (□((∀ q, q.[κ] ={lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={lftN}=∗ q.[κ])) ∗
+     ([†κ'] ={lftN}=∗ [†κ])))%I.
 
-Infix "⊑" := lft_incl (at level 60, right associativity) : C_scope.
+Infix "⊑" := lft_incl (at level 60) : C_scope.
 
 Section incl.
-  Context `{lifetimeG Σ}.
+  Context `{invG Σ, lifetimeG Σ}.
 
   Global Instance lft_incl_persistent κ κ': PersistentP (κ ⊑ κ') := _.
 
   Lemma lft_incl_acc `(nclose lftN ⊆ E) κ κ' q:
     κ ⊑ κ' ⊢ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
   Proof.
-    iIntros "#H Hq". iApply fupd_mask_mono. eassumption.
+    iIntros "#[H _] Hq". iApply fupd_mask_mono. eassumption.
     iMod ("H" with "*Hq") as (q') "[Hq' Hclose]". iExists q'.
     iIntros "{$Hq'}!>Hq". iApply fupd_mask_mono. eassumption. by iApply "Hclose".
   Qed.
 
+  Lemma lft_incl_dead `(nclose lftN ⊆ E) κ κ': κ ⊑ κ' ⊢ [†κ'] ={E}=∗ [†κ].
+  Proof.
+    iIntros "#[_ H] Hq". iApply fupd_mask_mono. eassumption. by iApply "H".
+  Qed.
+
   Lemma lft_le_incl κ κ': κ' ≼ κ → True ⊢ κ ⊑ κ'.
   Proof.
-    iIntros ([κ0 ->%leibniz_equiv]) "!#*[Hκ' Hκ0]". iExists q.
-    iIntros "!>{$Hκ'}Hκ'!>". by iSplitR "Hκ0".
+    iIntros ([κ0 ->%leibniz_equiv]) "!#". iSplitR.
+    - iIntros (q) "[Hκ' Hκ0]". iExists q. iIntros "!>{$Hκ'}Hκ'!>". by iSplitR "Hκ0".
+    - iIntros "?!>". iApply lft_dead_or. auto.
   Qed.
 
-  Lemma lft_incl_relf κ : True ⊢ κ ⊑ κ.
+  Lemma lft_incl_refl κ : True ⊢ κ ⊑ κ.
   Proof. by apply lft_le_incl. Qed.
 
   Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ∗ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
   Proof.
-    unfold lft_incl. iIntros "[#H1 #H2]!#*Hκ".
-    iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
-    iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
-    iExists q''. iIntros "{$Hκ''}!>Hκ''". iMod ("Hclose'" with "Hκ''") as "Hκ'".
-    by iApply "Hclose".
+    unfold lft_incl. iIntros "[#[H1 H1†] #[H2 H2†]]!#". iSplitR.
+    - iIntros (q) "Hκ".
+      iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
+      iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
+      iExists q''. iIntros "{$Hκ''}!>Hκ''". iMod ("Hclose'" with "Hκ''") as "Hκ'".
+        by iApply "Hclose".
+    - iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
   Qed.
 
-  Axiom lft_idx_borrow_shorten :
-    ∀ κ κ' i P, κ ⊑ κ' ⊢ lft_idx_borrow κ' i P -∗ lft_idx_borrow κ i P.
+  Axiom idx_borrow_shorten :
+    ∀ κ κ' i P, κ ⊑ κ' ⊢ idx_borrow κ' i P -∗ idx_borrow κ i P.
 
-  Lemma lft_borrow_shorten κ κ' P: κ ⊑ κ' ⊢ &{κ'}P -∗ &{κ}P.
+  Lemma borrow_shorten κ κ' P: κ ⊑ κ' ⊢ &{κ'}P -∗ &{κ}P.
   Proof.
-    iIntros "H⊑ H". unfold lft_borrow. iDestruct "H" as (i) "[??]".
-    iExists i. iFrame. by iApply (lft_idx_borrow_shorten with "H⊑").
+    iIntros "H⊑ H". unfold borrow. iDestruct "H" as (i) "[??]".
+    iExists i. iFrame. by iApply (idx_borrow_shorten with "H⊑").
   Qed.
 
   Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' ∗ κ ⊑ κ'' ⊢ κ ⊑ κ' ⋅ κ''.
   Proof.
-    iIntros "[#H⊑1 #H⊑2]!#". iIntros (q). iIntros "[Hκ'1 Hκ'2]".
-    iMod ("H⊑1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
-    iMod ("H⊑2" with "*Hκ'2") as (q'') "[Hκ'' Hclose'']".
-    destruct (Qp_lower_bound q' q'') as (qq & q'0 & q''0 & -> & ->).
-    iExists qq. rewrite -lft_own_op !lft_own_frac_op.
-    iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
-    iIntros "!>[Hκ'0 Hκ''0]".
-    iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
-    by iMod ("Hclose''" with "[$Hκ'' $Hκ''0]") as "$".
+    iIntros "[#[H1 H1†] #[H2 H2†]]!#". iSplitR.
+    - iIntros (q) "[Hκ'1 Hκ'2]".
+      iMod ("H1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
+      iMod ("H2" with "*Hκ'2") as (q'') "[Hκ'' Hclose'']".
+      destruct (Qp_lower_bound q' q'') as (qq & q'0 & q''0 & -> & ->).
+      iExists qq. rewrite -lft_own_op !lft_own_frac_op.
+      iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
+      iIntros "!>[Hκ'0 Hκ''0]".
+      iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
+      by iMod ("Hclose''" with "[$Hκ'' $Hκ''0]") as "$".
+    - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
   Qed.
 
   Lemma lft_incl_static κ : True ⊢ κ ⊑ static.
   Proof.
-    iIntros "!#*$". iExists 1%Qp. iSplitR.
-    iApply lft_own_static. auto.
+    iIntros "!#". iSplitR.
+    - iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_own_static. auto.
+    - iIntros "?". by iDestruct (lft_not_dead_static with "[-]") as "[]".
   Qed.
 
-  Lemma lft_reborrow `(nclose lftN ⊆ E) P κ κ':
-    κ' ⊑ κ ⊢ &{κ}P ={E}=∗ &{κ'}P ∗ κ' ∋ &{κ}P.
+  Lemma reborrow `(nclose lftN ⊆ E) P κ κ':
+    κ' ⊑ κ ⊢ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
   Proof.
-    iIntros "#H⊑ HP". iMod (lft_reborrow_static with "HP") as "[Hκ' H∋]".
+    iIntros "#H⊑ HP". iMod (borrow_reborrow' with "HP") as "[Hκ' H∋]".
       done. by exists κ'.
-    iDestruct (lft_borrow_shorten with "[H⊑] Hκ'") as "$".
-    { iApply lft_incl_lb. iSplit. done. iIntros "!#*". iApply lft_incl_relf. }
-    iApply lft_extract_mono; last by iFrame; auto. exists κ. by rewrite comm.
+    iDestruct (borrow_shorten with "[H⊑] Hκ'") as "$".
+    { iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
+    iIntros "!>Hκ'". iApply ("H∋" with "[Hκ']"). iApply lft_dead_or. auto.
   Qed.
 
 End incl.
@@ -347,76 +354,107 @@ Typeclasses Opaque lft_incl.
 (*** Derived notions  *)
 
 (** Shared borrows  *)
-Definition lft_shr_borrow `{lifetimeG Σ} κ (P : iProp Σ) :=
-  (∃ i, lft_idx_borrow κ i P ∗ lft_idx_borrow_persist i)%I.
-Notation "&shr{ κ } P" := (lft_shr_borrow κ P)
+Definition shr_borrow `{invG Σ, lifetimeG Σ} κ (P : iProp Σ) :=
+  (∃ i, idx_borrow κ i P ∗ inv lftN (∃ q, idx_borrow_own q i))%I.
+Notation "&shr{ κ } P" := (shr_borrow κ P)
   (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope.
 
 Section shared_borrows.
-  Context `{lifetimeG Σ} (P : iProp Σ).
+  Context `{invG Σ, lifetimeG Σ} (P : iProp Σ).
 
-  Global Instance lft_shr_borrow_proper :
-    Proper ((⊣⊢) ==> (⊣⊢)) (lft_shr_borrow κ).
+  Global Instance shr_borrow_proper :
+    Proper ((⊣⊢) ==> (⊣⊢)) (shr_borrow κ).
   Proof. solve_proper. Qed.
-  Global Instance lft_shr_borrow_persistent : PersistentP (&shr{κ} P) := _.
+  Global Instance shr_borrow_persistent : PersistentP (&shr{κ} P) := _.
+
+  Lemma borrow_share `(nclose lftN ⊆ E) κ : &{κ}P ={E}=∗ &shr{κ}P.
+  Proof.
+    iIntros "HP". unfold borrow. iDestruct "HP" as (i) "(#?&Hown)".
+    iExists i. iFrame "#". iApply inv_alloc. auto.
+  Qed.
 
-  Lemma lft_borrow_share `(nclose lftN ⊆ E) κ : &{κ}P ={E}=∗ &shr{κ}P.
+  Lemma shr_borrow_acc `(nclose lftN ⊆ E) κ :
+    &shr{κ}P ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ True) ∨
+                          [†κ] ∗ |={E∖lftN,E}=> True.
   Proof.
-    iIntros "HP". unfold lft_borrow. iDestruct "HP" as (i) "(#?&Hown)".
-    iExists i. iMod (lft_idx_borrow_persist_upd with "[$Hown]"). done. by auto.
+    iIntros "#HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
+    iInv lftN as (q') ">Hq'" "Hclose".
+    rewrite -(Qp_div_2 q') /idx_borrow_own -op_singleton auth_frag_op own_op.
+    iDestruct "Hq'" as "[Hq'0 Hq'1]". iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
+    iMod (idx_borrow_atomic_acc with "Hidx Hq'0") as "[[HP Hclose]|[H† Hclose]]". done.
+    - iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
+    - iRight. iFrame. iIntros "!>". by iMod "Hclose".
   Qed.
 
-  Lemma lft_shr_borrow_acc `(nclose lftN ⊆ E) q κ :
+  Lemma shr_borrow_acc_tok `(nclose lftN ⊆ E) q κ :
     &shr{κ}P ⊢ q.[κ] ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ q.[κ]).
   Proof.
-    iIntros "#HP Hκ". iDestruct "HP" as (i) "(#Hidx&#Hpers)".
-    iMod (lft_idx_borrow_persist_acc with "Hidx Hpers Hκ") as "[$H]". done.
-    iApply "H".
+    iIntros "#Hshr Hκ". iMod (shr_borrow_acc with "Hshr") as "[[$ Hclose]|[H† _]]". done.
+    - iIntros "!>HP". by iMod ("Hclose" with "HP").
+    - iDestruct (lft_own_dead with "[-]") as "[]". by iFrame.
   Qed.
 
-  Lemma lft_shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -∗ &shr{κ}P.
+  Lemma shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -∗ &shr{κ}P.
   Proof.
     iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
-      by iApply (lft_idx_borrow_shorten with "H⊑").
+      by iApply (idx_borrow_shorten with "H⊑").
   Qed.
 
 End shared_borrows.
 
-Typeclasses Opaque lft_shr_borrow.
+Typeclasses Opaque shr_borrow.
 
 (** Fractured borrows  *)
-Definition lft_frac_borrow `{lifetimeG Σ} κ (Φ : Qp → iProp Σ) :=
+Definition frac_borrow `{invG Σ, lifetimeG Σ} κ (Φ : Qp → iProp Σ) :=
   (∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗
                        (q = 1%Qp ∨ ∃ q', (q + q')%Qp = 1%Qp ∗ q'.[κ']))%I.
-Notation "&frac{ κ } P" := (lft_frac_borrow κ P)
+Notation "&frac{ κ } P" := (frac_borrow κ P)
   (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
 
 Section frac_borrow.
 
-  Context `{lifetimeG Σ}.
+  Context `{invG Σ, lifetimeG Σ}.
+
+  Global Instance frac_borrow_proper :
+    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_borrow κ).
+  Proof. solve_proper. Qed.
+  Global Instance frac_borrow_persistent : PersistentP (&frac{κ}φ) := _.
 
-  Lemma lft_borrow_fracture `(nclose lftN ⊆ E) q κ φ:
+  (* FIXME : we shall not use tokens for κ here. *)
+  Lemma borrow_fracture φ `(nclose lftN ⊆ E) q κ:
     &{κ}(φ 1%Qp) ∗ q.[κ] ={E}=∗ &frac{κ}φ ∗ q.[κ].
   Proof.
     iIntros "[Hφ Hκ]". iMod (own_alloc 1%Qp) as (γ) "?". done.
-    iMod (lft_borrow_acc_strong with "Hφ Hκ") as "[Hφ Hclose]". done.
+    iMod (borrow_acc_strong with "Hφ Hκ") as "[Hφ Hclose]". done.
     iMod ("Hclose" with "*[-]") as "[Hφ$]"; last first.
-    { iExists γ, κ. iSplitR; last by iApply (lft_borrow_share with "Hφ").
-      iApply lft_incl_relf. }
+    { iExists γ, κ. iSplitR; last by iApply (borrow_share with "Hφ").
+      iApply lft_incl_refl. }
     iSplitL. by iExists 1%Qp; iFrame; auto.
     iIntros "!>[H† Hφ]!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
     iDestruct "Hκ" as (q'') "[_ Hκ]".
     iDestruct (lft_own_dead with "[$Hκ $H†]") as "[]".
   Qed.
 
-  Lemma lft_frac_borrow_acc `(nclose lftN ⊆ E) q κ φ:
+  Lemma frac_borrow_atomic_acc `(nclose lftN ⊆ E) κ φ:
+    &frac{κ}φ ={E,E∖lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖lftN,E}=∗ True))
+                          ∨ [†κ] ∗ |={E∖lftN,E}=> True.
+  Proof.
+    iIntros "#Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
+    iMod (shr_borrow_acc with "Hshr") as "[[Hφ Hclose]|[H† Hclose]]". done.
+    - iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
+      iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
+    - iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
+      iApply fupd_intro_mask. set_solver. done.
+  Qed.
+
+  Lemma frac_borrow_acc `(nclose lftN ⊆ E) q κ φ:
     □ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) ⊢
     &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
   Proof.
-    iIntros "#Hφ Hfrac Hκ". unfold lft_frac_borrow.
+    iIntros "#Hφ Hfrac Hκ". unfold frac_borrow.
     iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
     iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done.
-    iMod (lft_shr_borrow_acc with "Hshr Hκ1") as "[H Hclose']". done.
+    iMod (shr_borrow_acc_tok with "Hshr Hκ1") as "[H Hclose']". done.
     iDestruct "H" as (qφ) "(Hφqφ & >Hown & Hq)".
     destruct (Qp_lower_bound (qκ'/2) (qφ/2)) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ).
     iExists qq.
@@ -432,7 +470,7 @@ Section frac_borrow.
         rewrite lft_own_frac_op. iIntros "{$Hκq $Hq'κ}!%".
         by rewrite assoc (comm _ _ qq) assoc -Hqφ Qp_div_2. }
     clear Hqφ qφ qφ0. iIntros "!>Hqφ".
-    iMod (lft_shr_borrow_acc with "Hshr Hκ1") as "[H Hclose']". done.
+    iMod (shr_borrow_acc_tok with "Hshr Hκ1") as "[H Hclose']". done.
     iDestruct "H" as (qφ) "(Hφqφ & >Hown & >[%|Hq])".
     { subst. iCombine "Hown" "Hownq" as "Hown".
       by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. }
@@ -455,43 +493,57 @@ Section frac_borrow.
       iApply "Hclose". rewrite -{2}(Qp_div_2 qκ') {2}Hqκ' !lft_own_frac_op. by iFrame.
   Qed.
 
-  Lemma lft_frac_borrow_shorten κ κ' φ: κ ⊑ κ' ⊢ &frac{κ'}φ -∗ &frac{κ}φ.
+  Lemma frac_borrow_shorten κ κ' φ: κ ⊑ κ' ⊢ &frac{κ'}φ -∗ &frac{κ}φ.
   Proof.
     iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[H⊑?]". iExists γ, κ0. iFrame.
     iApply lft_incl_trans. iFrame.
   Qed.
 
+  Lemma frac_borrow_incl κ κ' q:
+    &frac{κ}(λ q', (q * q').[κ']) ⊢ κ ⊑ κ'.
+  Proof.
+    iIntros "#Hbor!#". iSplitR.
+    - iIntros (q') "Hκ'".
+      iMod (frac_borrow_acc with "[] Hbor Hκ'") as (q'') "[>? Hclose]". done.
+      + iIntros "/=!#*". rewrite Qp_mult_plus_distr_r lft_own_frac_op. iSplit; auto.
+      + iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
+    - iIntros "H†'".
+      iMod (frac_borrow_atomic_acc with "Hbor") as "[H|[$ $]]". done.
+      iDestruct "H" as (q') "[>Hκ' _]".
+      iDestruct (lft_own_dead with "[$H†' $Hκ']") as "[]".
+  Qed.
+
 End frac_borrow.
 
-Typeclasses Opaque lft_frac_borrow.
+Typeclasses Opaque frac_borrow.
 
 (** Thread local borrows  *)
 
-Definition lft_tl_borrow `{lifetimeG Σ, thread_localG Σ}
+Definition tl_borrow `{invG Σ, lifetimeG Σ, thread_localG Σ}
            (κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
-  (∃ i, lft_idx_borrow κ i P ∗ tl_inv tid N (lft_idx_borrow_own i))%I.
+  (∃ i, idx_borrow κ i P ∗ tl_inv tid N (idx_borrow_own 1 i))%I.
 
-Notation "&tl{ κ | tid | N } P" := (lft_tl_borrow κ tid N P)
+Notation "&tl{ κ | tid | N } P" := (tl_borrow κ tid N P)
   (format "&tl{ κ | tid | N } P", at level 20, right associativity) : uPred_scope.
 
-Section tl_borrows.
-  Context `{lifetimeG Σ, thread_localG Σ}
+Section tl_borrow.
+  Context `{invG Σ, lifetimeG Σ, thread_localG Σ}
           (tid : thread_id) (N : namespace) (P : iProp Σ).
 
-  Global Instance lft_tl_borrow_persistent κ : PersistentP (&tl{κ|tid|N} P) := _.
-  Global Instance lft_tl_borrow_proper κ :
-    Proper ((⊣⊢) ==> (⊣⊢)) (lft_tl_borrow κ tid N).
+  Global Instance tl_borrow_persistent κ : PersistentP (&tl{κ|tid|N} P) := _.
+  Global Instance tl_borrow_proper κ :
+    Proper ((⊣⊢) ==> (⊣⊢)) (tl_borrow κ tid N).
   Proof.
     intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
   Qed.
 
-  Lemma lft_borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ|tid|N}P.
+  Lemma borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ|tid|N}P.
   Proof.
-    iIntros "HP". unfold lft_borrow. iDestruct "HP" as (i) "[#? Hown]".
+    iIntros "HP". unfold borrow. iDestruct "HP" as (i) "[#? Hown]".
     iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
   Qed.
 
-  Lemma lft_tl_borrow_acc q κ E F :
+  Lemma tl_borrow_acc q κ E F :
     nclose lftN ⊆ E → nclose tlN ⊆ E → nclose N ⊆ F →
     &tl{κ|tid|N}P ⊢ q.[κ] ∗ tl_own tid F ={E}=∗ ▷P ∗ tl_own tid (F ∖ N) ∗
                      (▷P ∗ tl_own tid (F ∖ N) ={E}=∗ q.[κ] ∗ tl_own tid F).
@@ -499,17 +551,17 @@ Section tl_borrows.
     iIntros (???) "#HP[Hκ Htlown]".
     iDestruct "HP" as (i) "(#Hpers&#Hinv)".
     iMod (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try done.
-    iMod (lft_idx_borrow_own_acc with "Hpers [$Hown $Hκ]") as "[HP Hclose']". done.
+    iMod (idx_borrow_acc with "Hpers [$Hown $Hκ]") as "[HP Hclose']". done.
     iIntros "{$HP $Htlown}!>[HP Htlown]".
     iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
   Qed.
 
-  Lemma lft_tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P.
+  Lemma tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P.
   Proof.
     iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
-    iApply (lft_idx_borrow_shorten with "Hκκ' H").
+    iApply (idx_borrow_shorten with "Hκκ' H").
   Qed.
 
-End tl_borrows.
+End tl_borrow.
 
-Typeclasses Opaque lft_tl_borrow.
+Typeclasses Opaque tl_borrow.
diff --git a/theories/memcpy.v b/theories/memcpy.v
index 18e414bea88c2f291a0ef6cd1f921be1c3fe56be..4fb6d9a2082cd800978fbecb70b91125c817b5c3 100644
--- a/theories/memcpy.v
+++ b/theories/memcpy.v
@@ -22,9 +22,9 @@ Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n:
   length vl1 = n → length vl2 = n →
   {{{ heap_ctx ∗ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
     #l1 <-{n} !#l2 @ E
-  {{{; #(), l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
+  {{{ RET #(); l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
 Proof.
-  iIntros (? Hvl1 Hvl2 Φ) "[(#Hinv & Hl1 & Hl2) HΦ]".
+  iIntros (? Hvl1 Hvl2 Φ) "(#Hinv & Hl1 & Hl2) HΦ".
   iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
   - iApply "HΦ". assert (n = O) by lia; subst.
     destruct vl1, vl2; try discriminate. by iFrame.
diff --git a/theories/perm.v b/theories/perm.v
index 0c75b87bdb2eeb5e1da3b1d25eb8a160815faa41..b925525ff10339e4b778d372ab47ff9c89dae9cf 100644
--- a/theories/perm.v
+++ b/theories/perm.v
@@ -24,10 +24,10 @@ Section perm.
     from_option (λ v, ty.(ty_own) tid [v]) False%I (eval_expr ν).
 
   Definition extract (κ : lifetime) (ρ : perm) : perm :=
-    λ tid, (κ ∋ ρ tid)%I.
+    λ tid, ([†κ] ={lftN}=∗ ▷ ρ tid)%I.
 
   Definition tok (κ : lifetime) (q : Qp) : perm :=
-    λ _, ([κ]{q} ∗ lft κ)%I.
+    λ _, q.[κ]%I.
 
   Definition incl (κ κ' : lifetime) : perm :=
     λ _, (κ ⊑ κ')%I.
@@ -53,9 +53,9 @@ Notation "v ◁ ty" := (has_type v ty)
 Notation "κ ∋ ρ" := (extract κ ρ)
   (at level 75, right associativity) : perm_scope.
 
-Notation "[ κ ]{ q }" := (tok κ q) (format "[ κ ]{ q }") : perm_scope.
+Notation "q .[ κ ]" := (tok κ q) (format "q .[ κ ]", at level 0) : perm_scope.
 
-Infix "⊑" := incl (at level 70) : perm_scope.
+Infix "⊑" := incl (at level 60) : perm_scope.
 
 Notation "∃ x .. y , P" :=
   (exist (λ x, .. (exist (λ y, P)) ..)) : perm_scope.
diff --git a/theories/perm_incl.v b/theories/perm_incl.v
index 5fd49048d8e30cd8c663de0a833a5fd730346eb1..2b1dce5aa8b3181f90b419ec9a33eb603e9df9d7 100644
--- a/theories/perm_incl.v
+++ b/theories/perm_incl.v
@@ -16,7 +16,7 @@ Section defs.
     λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
 
   Definition borrowing κ (ρ ρ1 ρ2 : perm) :=
-    ∀ tid, lft κ ⊢ ρ tid -∗ ρ1 tid ={⊤}=∗ ρ2 tid ∗ κ ∋ ρ1 tid.
+    ∀ tid, ρ tid ⊢ ρ1 tid ={⊤}=∗ ρ2 tid ∗ (κ ∋ ρ1)%P tid.
 
 End defs.
 
@@ -93,8 +93,7 @@ Section props.
   Lemma perm_tok_plus κ q1 q2 :
     tok κ q1 ∗ tok κ q2 ⇔ tok κ (q1 + q2).
   Proof.
-    rewrite /tok /sep /=; split; intros tid; rewrite -lft_own_op;
-      iIntros "[[$$]H]!>". by iDestruct "H" as "[$?]". by auto.
+    rewrite /tok /sep /=; split; iIntros (tid) "?"; rewrite lft_own_frac_op //.
   Qed.
 
   Lemma perm_lftincl_refl κ : ⊤ ⇒ κ ⊑ κ.
@@ -104,7 +103,7 @@ Section props.
   Proof. iIntros (tid) "[#?#?]!>". iApply lft_incl_trans. auto. Qed.
 
   Lemma perm_incl_share q ν κ ty :
-    ν ◁ &uniq{κ} ty ∗ [κ]{q} ⇒ ν ◁ &shr{κ} ty ∗ [κ]{q}.
+    ν ◁ &uniq{κ} ty ∗ q.[κ] ⇒ ν ◁ &shr{κ} ty ∗ q.[κ].
   Proof.
     iIntros (tid) "[Huniq [Htok $]]". unfold has_type.
     destruct (eval_expr ν); last by iDestruct "Huniq" as "[]".
@@ -188,7 +187,7 @@ Section props.
     rewrite split_prod_mt.
     iInduction (combine_offs tyl 0) as [|[ty offs] ll] "IH". by auto.
     rewrite big_sepL_cons /=.
-    iMod (lft_borrow_split with "H") as "[H0 H]". set_solver.
+    iMod (borrow_split with "H") as "[H0 H]". set_solver.
     iMod ("IH" with "H") as "$". iModIntro. iExists _. eauto.
   Qed.
 
@@ -215,39 +214,37 @@ Section props.
   Lemma borrowing_perm_incl κ ρ ρ1 ρ2 θ :
     borrowing κ ρ ρ1 ρ2 → ρ ∗ κ ∋ θ ∗ ρ1 ⇒ ρ2 ∗ κ ∋ (θ ∗ ρ1).
   Proof.
-    iIntros (Hbor tid) "(Hρ&Hθ&Hρ1)".
-    iMod (Hbor with "[#] Hρ Hρ1") as "[$ ?]". by iApply lft_extract_lft.
-    iApply lft_extract_combine. set_solver. by iFrame.
+    iIntros (Hbor tid) "(Hρ&Hθ&Hρ1)". iMod (Hbor with "Hρ Hρ1") as "[$ Hρ1]".
+    iIntros "!>#H†". iSplitL "Hθ". by iApply "Hθ". by iApply "Hρ1".
   Qed.
 
   Lemma own_uniq_borrowing ν q ty κ :
     borrowing κ ⊤ (ν ◁ own q ty) (ν ◁ &uniq{κ} ty).
   Proof.
-    iIntros (tid) "#Hκ _ Hown". unfold has_type.
+    iIntros (tid) "_ Hown". unfold has_type.
     destruct (eval_expr ν) as [[[|l|]|]|];
       try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
     iDestruct "Hown" as (l') "[EQ [Hf Hown]]". iDestruct "EQ" as %[=]. subst l'.
-    iMod (lft_borrow_create with "Hκ Hown") as "[Hbor Hext]". done.
+    iApply (fupd_mask_mono lftN). done.
+    iMod (borrow_create with "Hown") as "[Hbor Hext]". done.
     iSplitL "Hbor". by simpl; eauto.
-    iMod (lft_borrow_create with "Hκ Hf") as "[_ Hf]". done.
-    iMod (lft_extract_combine with "[$Hext $Hf]"). done.
-    iModIntro. iApply lft_extract_mono; last done.
-    iIntros "H/=". iExists _. iSplit. done. by iDestruct "H" as "[$$]".
+    iMod (borrow_create with "Hf") as "[_ Hf]". done.
+    iIntros "!>#H†".
+    iMod ("Hext" with "H†") as "Hext". iMod ("Hf" with "H†") as "Hf". iIntros "!>/=".
+    iExists _. iFrame. auto.
   Qed.
 
   Lemma reborrow_uniq_borrowing κ κ' ν ty :
     borrowing κ (κ ⊑ κ') (ν ◁ &uniq{κ'}ty) (ν ◁ &uniq{κ}ty).
   Proof.
-    iIntros (tid) "_ #Hord H". unfold has_type.
+    iIntros (tid) "#Hord H". unfold has_type.
     destruct (eval_expr ν) as [[[|l|]|]|];
       try by (iDestruct "H" as "[]" || iDestruct "H" as (l) "[% _]").
     iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. subst l'.
-    iMod (lft_reborrow with "Hord H") as "[H Hextr]". done.
+    iApply (fupd_mask_mono lftN). done.
+    iMod (reborrow with "Hord H") as "[H Hextr]". done.
     iModIntro. iSplitL "H". iExists _. by eauto.
-    iApply (lft_extract_proper with "Hextr").
-    iSplit; iIntros "H/=".
-    - iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. by subst l'.
-    - iExists _. eauto.
+    iIntros "H†". iMod ("Hextr" with "H†"). simpl. auto.
   Qed.
 
   Lemma reborrow_shr_perm_incl κ κ' ν ty :
@@ -261,12 +258,25 @@ Section props.
     by iApply (ty_shr_mono with "Hord Hκ'").
   Qed.
 
-  Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ [κ']{q} (κ ⊑ κ').
-  Proof.
-    iIntros (tid) "#Hκ #Hord [Htok #Hκ']".
-    iMod (lft_mkincl' with "[#] Htok") as "[$ H]". done. by iFrame "#".
-    iMod (lft_borrow_create with "Hκ []") as "[_ H']". done. by iNext; iApply "Hκ'".
-    iApply lft_extract_combine. done. by iFrame.
-  Qed.
+  (* TODO *)
+  (* Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ q.[κ'] (κ ⊑ κ'). *)
+  (* Proof. *)
+  (*   iIntros (tid) "_ Htok". iApply fupd_mask_mono. done. *)
+  (*   iDestruct "Htok" as "[Htok1 Htok2]". *)
+  (*   iMod (borrow_create with "[Htok1]") as "[Hbor Hclose]". reflexivity. *)
+  (*   { iIntros "!>". iExact "Htok1". } *)
+  (*   iMod (borrow_fracture (λ q', (q / 2 * q').[κ'])%I with "[Hbor $Htok2]") *)
+  (*     as "[Hbor Htok]". done. *)
+  (*   { by rewrite Qp_mult_1_r. } *)
+  (*   iIntros "{$Htok}!>". iSplitL "Hbor". *)
+  (*   iApply frac_borrow_incl. done. frac_borrow_incl *)
+
+  (*     iExact "Hclose". iFrame. *)
+
+  (*   iMod (frac_borrow_incl with "[-]"). *)
+  (*   iMod (lft_mkincl' with "[#] Htok") as "[$ H]". done. by iFrame "#". *)
+  (*   iMod (lft_borrow_create with "Hκ []") as "[_ H']". done. by iNext; iApply "Hκ'". *)
+  (*   iApply lft_extract_combine. done. by iFrame. *)
+  (* Qed. *)
 
 End props.
diff --git a/theories/type.v b/theories/type.v
index 029c5090e66f1efe316d29a065704cd34eba4508..3b4c221b006ce00938057197a537748a3901e1db 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -33,14 +33,14 @@ Record type `{heapG Σ, lifetimeG Σ, thread_localG Σ} :=
        more consistent with thread-local tokens, which we do not
        give any. *)
     ty_share E N κ l tid q : mgmtE ⊥ nclose N → mgmtE ⊆ E →
-      &{κ} (l ↦∗: ty_own tid) ⊢ [κ]{q} ={E}=∗ ty_shr κ tid N l ∗ [κ]{q};
+      &{κ} (l ↦∗: ty_own tid) ⊢ q.[κ] ={E}=∗ ty_shr κ tid N l ∗ q.[κ];
     ty_shr_mono κ κ' tid N l :
       κ' ⊑ κ ⊢ ty_shr κ tid N l → ty_shr κ' tid N l;
     ty_shr_acc κ tid E N l q :
       ty_dup → mgmtE ∪ nclose N ⊆ E →
       ty_shr κ tid N l ⊢
-        [κ]{q} ∗ tl_own tid N ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
-           (▷l ↦∗{q'}: ty_own tid ={E}=∗ [κ]{q} ∗ tl_own tid N)
+        q.[κ] ∗ tl_own tid N ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
+           (▷l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ tl_own tid N)
   }.
 Global Existing Instances ty_shr_persistent ty_dup_persistent.
 
@@ -66,20 +66,22 @@ Program Coercion ty_of_st `{heapG Σ, lifetimeG Σ, thread_localG Σ}
 Next Obligation. intros. apply st_size_eq. Qed.
 Next Obligation.
   intros Σ ??? st E N κ l tid q ??. iIntros "Hmt Htok".
-  iMod (lft_borrow_exists with "Hmt Htok") as (vl) "[Hmt Htok]". set_solver.
-  iMod (lft_borrow_split with "Hmt") as "[Hmt Hown]". set_solver.
-  iMod (lft_borrow_persistent with "Hown Htok") as "[Hown $]". set_solver.
-  iExists vl. iFrame. by iApply lft_borrow_fracture.
+  iMod (borrow_exists with "Hmt Htok") as (vl) "[Hmt Htok]". set_solver.
+  iMod (borrow_split with "Hmt") as "[Hmt Hown]". set_solver.
+  iMod (borrow_persistent with "Hown Htok") as "[Hown Htok]". set_solver.
+  iMod (borrow_fracture with "[Hmt $Htok]") as "[Hfrac $]"; last first.
+  { iExists vl. by iFrame. }
+  done. set_solver.
 Qed.
 Next Obligation.
   intros Σ???. iIntros (st κ κ' tid N l) "#Hord H".
   iDestruct "H" as (vl) "[Hf Hown]".
-  iExists vl. iFrame. by iApply (lft_frac_borrow_incl with "Hord").
+  iExists vl. iFrame. by iApply (frac_borrow_shorten with "Hord").
 Qed.
 Next Obligation.
   intros Σ??? st κ tid N E l q ??.  iIntros "#Hshr[Hlft $]".
   iDestruct "Hshr" as (vl) "[Hf Hown]".
-  iMod (lft_frac_borrow_open with "[] Hf Hlft") as (q') "[Hmt Hclose]";
+  iMod (frac_borrow_acc with "[] Hf Hlft") as (q') "[Hmt Hclose]";
     first set_solver.
   - iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_vec_op_eq.
     iSplit; auto.
@@ -112,9 +114,9 @@ Section types.
   Next Obligation. iIntros (tid vl) "[]". Qed.
   Next Obligation.
     iIntros (????????) "Hb Htok".
-    iMod (lft_borrow_exists with "Hb Htok") as (vl) "[Hb Htok]". set_solver.
-    iMod (lft_borrow_split with "Hb") as "[_ Hb]". set_solver.
-    iMod (lft_borrow_persistent with "Hb Htok") as "[>[] _]". set_solver.
+    iMod (borrow_exists with "Hb Htok") as (vl) "[Hb Htok]". set_solver.
+    iMod (borrow_split with "Hb") as "[_ Hb]". set_solver.
+    iMod (borrow_persistent with "Hb Htok") as "[>[] _]". set_solver.
   Qed.
   Next Obligation. iIntros (?????) "_ []". Qed.
   Next Obligation. intros. iIntros "[]". Qed.
@@ -146,7 +148,7 @@ Section types.
                                ∗ ▷ l ↦∗: ty.(ty_own) tid)%I;
        ty_shr κ tid N l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
-            ∀ q', □ ([κ]{q'} ={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) κ tid N l' ∗ [κ]{q'}))%I
+            ∀ q', □ (q'.[κ] ={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) κ tid N l' ∗ q'.[κ]))%I
     |}.
   Next Obligation. done. Qed.
   Next Obligation.
@@ -154,36 +156,36 @@ Section types.
   Qed.
   Next Obligation.
     move=> q ty E N κ l tid q' ?? /=. iIntros "Hshr Htok".
-    iMod (lft_borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
-    iMod (lft_borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (lft_borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
-    iMod (lft_borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
-    iMod (lft_borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
+    iMod (borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
+    iMod (borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
+    iMod (borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
+    iMod (borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
+    iMod (borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
     rewrite heap_mapsto_vec_singleton.
-    iMod (lft_borrow_split with "Hb2") as "[_ Hb2]". set_solver.
-    iMod (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf".
-    rewrite lft_borrow_persist. iDestruct "Hb2" as (κ0 i) "(#Hord&#Hpb&Hpbown)".
-    iMod (inv_alloc N _ (lft_pers_borrow_own i κ0 ∨ ty_shr ty κ tid N l')%I
+    iMod (borrow_split with "Hb2") as "[_ Hb2]". set_solver.
+    iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "[$Hb1 $Htok]") as "[Hbf $]".
+      set_solver.
+    rewrite /borrow. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
+    iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty κ tid N l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
-    iIntros "!>{$Htok}". iExists l'. iFrame. iIntros (q'') "!#Htok".
+    iExists l'. iIntros "!>{$Hbf}".  iIntros (q'') "!#Htok".
     iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
     replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (&{κ}▷ l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
-      { iApply lft_borrow_persist. eauto. }
-      iMod (lft_borrow_open with "Hb Htok") as "[Hown Hob]". set_solver.
+      { rewrite /borrow. iExists i. eauto. }
+      iMod (borrow_acc_strong with "Hb Htok") as "[Hown Hclose']". set_solver.
       iIntros "!>". iNext.
-      iMod (lft_borrow_close_stronger with "Hown Hob []") as "[Hb Htok]".
-        set_solver. eauto 10.
+      iMod ("Hclose'" with "*[Hown]") as "[Hb Htok]". iFrame. by iIntros "!>[?$]".
       iMod (ty.(ty_share) with "Hb Htok") as "[#Hshr Htok]"; try done.
       iMod ("Hclose" with "[]") as "_"; by eauto.
     - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
   Qed.
   Next Obligation.
     iIntros (_ ty κ κ' tid N l) "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]".
-    iExists l'. iSplit. by iApply (lft_frac_borrow_incl with "[]").
+    iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]").
     iIntros (q') "!#Htok".
-    iMod (lft_incl_trade with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
+    iMod (lft_incl_acc with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
     iMod ("Hvs" $! q'' with "Htok") as "Hvs'".
     iIntros "!>". iNext. iMod "Hvs'" as "[Hshr Htok]".
     iMod ("Hclose" with "Htok"). iFrame.
@@ -197,8 +199,8 @@ Section types.
          (∃ l:loc, vl = [ #l ] ∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
        ty_shr κ' tid N l :=
          (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
-            ∀ q' κ'', □ (κ'' ⊑ κ ∗ κ'' ⊑ κ' ∗ [κ'']{q'}
-               ={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) κ'' tid N l' ∗ [κ'']{q'}))%I
+            ∀ q', □ (q'.[κ ⋅ κ']
+               ={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) (κ⋅κ') tid N l' ∗ q'.[κ⋅κ']))%I
     |}.
   Next Obligation. done. Qed.
   Next Obligation.
@@ -206,50 +208,41 @@ Section types.
   Qed.
   Next Obligation.
     move=> κ ty E N κ' l tid q' ??/=. iIntros "Hshr Htok".
-    iMod (lft_borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
-    iMod (lft_borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (lft_borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
-    iMod (lft_borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
-    iMod (lft_borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
+    iMod (borrow_exists with "Hshr Htok") as (vl) "[Hb Htok]". set_solver.
+    iMod (borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
+    iMod (borrow_exists with "Hb2 Htok") as (l') "[Hb2 Htok]". set_solver.
+    iMod (borrow_split with "Hb2") as "[EQ Hb2]". set_solver.
+    iMod (borrow_persistent with "EQ Htok") as "[>% Htok]". set_solver. subst.
     rewrite heap_mapsto_vec_singleton.
-    iMod (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf".
-    rewrite lft_borrow_persist.
-    iDestruct "Hb2" as (κ0 i) "(#Hord&#Hpb&Hpbown)".
-    iMod (inv_alloc N _ (lft_pers_borrow_own i κ0 ∨ ty_shr ty κ' tid N l')%I
+    iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "[$Hb1 $Htok]")
+      as "[Hbf $]". set_solver.
+    rewrite {1}/borrow. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
+    iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty (κ⋅κ') tid N l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
-    iIntros "!>{$Htok}". iExists l'. iFrame.
-    iIntros (q'' κ'') "!#(#Hκ''κ & #Hκ''κ' & Htok)".
+    iExists l'. iIntros "!>{$Hbf}". iIntros (q'') "!#Htok".
     iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
     replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iAssert (&{κ''}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
-      { iApply lft_borrow_persist. iExists κ0, i. iFrame "∗ #".
-        iApply lft_incl_trans. eauto. }
-      iMod (lft_borrow_open with "Hb Htok") as "[Hown Hob]". set_solver.
-      iIntros "!>". iNext.
-      iMod (lft_borrow_unnest with "Hκ''κ [$Hown $Hob]") as "[Htok Hb]". set_solver.
+    - iAssert (&{κ'}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
+      { rewrite /borrow. eauto. }
+      iMod (borrow_unnest with "Hb") as "Hb". set_solver.
+      iIntros "!>". iNext. iMod "Hb".
       iMod (ty.(ty_share) with "Hb Htok") as "[#Hshr Htok]"; try done.
-      iMod ("Hclose" with "[]") as "_".
-      (* FIXME : the "global sharing protocol" that we used for [own]
-         does not work here, because we do not know at the beginning
-         at which lifetime we will need the sharing.
-
-         This seems somewhat similar to the RefCell problem: we would
-         need a lifetime that would be the union of κ and κ'. *)
-      admit.
-      by eauto.
-    - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_". by eauto.
-      iIntros "!>{$Htok}". by iApply (ty.(ty_shr_mono) with "Hκ''κ'").
-  Admitted.
+      iMod ("Hclose" with "[]") as "_". eauto. by iFrame.
+    - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
+  Qed.
   Next Obligation.
     iIntros (κ0 ty κ κ' tid N l) "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]".
-    iExists l'. iSplit. by iApply (lft_frac_borrow_incl with "[]").
-    iIntros (q' κ'') "!#(#Hκ0 & #Hκ' & Htok)".
-    iMod ("Hvs" $! q' κ'' with "[Htok]") as "Hclose".
-    { iFrame. iSplit. done. iApply lft_incl_trans. eauto. }
-    iIntros "!>". iNext. iMod "Hclose" as "[Hshr Htok]".
-    iIntros "!>{$Htok}". iApply (ty.(ty_shr_mono) with "[] Hshr").
-    iApply lft_incl_refl.
+    iAssert (κ0⋅κ' ⊑ κ0⋅κ) as "#Hκ0".
+    { iApply lft_incl_lb. iSplit.
+      - iApply lft_le_incl. by exists κ'.
+      - iApply lft_incl_trans. iSplit; last done.
+        iApply lft_le_incl. exists κ0. apply (comm _). }
+    iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]"). iIntros (q) "!#Htok".
+    iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]". set_solver.
+    iMod ("Hvs" $! q' with "Htok") as "Hclose'".  iIntros "!>". iNext.
+    iMod "Hclose'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
+    by iApply (ty_shr_mono with "Hκ0").
   Qed.
   Next Obligation. done. Qed.
 
@@ -358,7 +351,7 @@ Section types.
     induction (combine_offs tyl 0) as [|[ty offs] ll IH].
     - iIntros (?) "_$!>". by rewrite big_sepL_nil.
     - iIntros (i) "Hown Htoks". rewrite big_sepL_cons.
-      iMod (lft_borrow_split with "Hown") as "[Hownh Hownq]". set_solver.
+      iMod (borrow_split with "Hown") as "[Hownh Hownq]". set_solver.
       iMod (IH (S i)%nat with "Hownq Htoks") as "[#Hshrq Htoks]".
       iMod (ty.(ty_share) _ (N .@ (i+0)%nat) with "Hownh Htoks") as "[#Hshrh $]".
         solve_ndisj. done.
@@ -392,8 +385,7 @@ Section types.
         instantiate (1:=λ _ y, _). simpl. reflexivity. }
       rewrite big_sepL_sepL. iDestruct "Hownq" as "[$ Hownq1]".
       iIntros "[Hh Hq]". rewrite (lft_own_split κ q).
-      iMod ("Hcloseh" with "[$Hh $Hownh1]") as "($&$)".
-      iApply "Hcloseq". by iFrame.
+      iMod ("Hcloseh" with "[$Hh $Hownh1]") as "[$$]". iApply "Hcloseq". by iFrame.
   Qed.
 
   Lemma split_sum_mt l tid q tyl :
@@ -402,10 +394,10 @@ Section types.
     ⊣⊢ ∃ (i : nat), l ↦{q} #i ∗ shift_loc l 1 ↦∗{q}: ty_own (nth i tyl emp) tid.
   Proof.
     iSplit; iIntros "H".
-    - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl') "(%&Hown)". subst.
+    - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl') "[% Hown]". subst.
       iExists i. iDestruct (heap_mapsto_vec_cons with "Hmt") as "[$ Hmt]".
       iExists vl'. by iFrame.
-    - iDestruct "H" as (i) "[Hmt1 Hown]". iDestruct "Hown" as (vl) "(Hmt2&Hown)".
+    - iDestruct "H" as (i) "[Hmt1 Hown]". iDestruct "Hown" as (vl) "[Hmt2 Hown]".
       iExists (#i::vl). rewrite heap_mapsto_vec_cons. iFrame. eauto.
   Qed.
 
@@ -445,22 +437,22 @@ Section types.
   Qed.
   Next Obligation.
     intros n tyl Hn E N κ l tid q ??. iIntros "Hown Htok". rewrite split_sum_mt.
-    iMod (lft_borrow_exists with "Hown Htok") as (i) "[Hown Htok]". set_solver.
-    iMod (lft_borrow_split with "Hown") as "[Hmt Hown]". set_solver.
-    iMod ((nth i tyl emp).(ty_share) with "Hown Htok") as "[#Hshr $]"; try done.
-    iExists i. iFrame "#". by iApply lft_borrow_fracture.
+    iMod (borrow_exists with "Hown Htok") as (i) "[Hown Htok]". set_solver.
+    iMod (borrow_split with "Hown") as "[Hmt Hown]". set_solver.
+    iMod ((nth i tyl emp).(ty_share) with "Hown Htok") as "[#Hshr Htok]"; try done.
+    iMod (borrow_fracture with "[-]") as "[H $]"; last by eauto. set_solver. iFrame.
   Qed.
   Next Obligation.
     intros n tyl Hn κ κ' tid N l. iIntros "#Hord H".
     iDestruct "H" as (i) "[Hown0 Hown]". iExists i. iSplitL "Hown0".
-    by iApply (lft_frac_borrow_incl with "Hord").
+    by iApply (frac_borrow_shorten with "Hord").
     by iApply ((nth i tyl emp).(ty_shr_mono) with "Hord").
   Qed.
   Next Obligation.
     intros n tyl Hn κ tid E N l q Hdup%Is_true_eq_true ?.
     iIntros "#H[[Htok1 Htok2] Htl]".
     setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
-    iMod (lft_frac_borrow_open with "[] Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
+    iMod (frac_borrow_acc with "[] Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
     { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; eauto. }
     iMod ((nth i tyl emp).(ty_shr_acc) with "Hshr [Htok2 $Htl]")
       as (q'2) "[Hownq Hclose']"; try done.
diff --git a/theories/type_incl.v b/theories/type_incl.v
index 82619adb7d8f89440e3505c2e5526e59a9fd6b18..5366276b7f58c26d47bf22ec41e40726755c490c 100644
--- a/theories/type_incl.v
+++ b/theories/type_incl.v
@@ -70,9 +70,19 @@ Section ty_incl.
   Proof.
     iIntros (tid) "#Hincl!>". iSplit; iIntros "!#*H".
     - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
-      by iApply (lft_borrow_incl with "Hincl").
-    - admit. (* TODO : fix the definition before *)
-  Admitted.
+      by iApply (borrow_shorten with "Hincl").
+    - iAssert (κ1 ⋅ κ ⊑ κ2 ⋅ κ) as "#Hincl'".
+      { iApply lft_incl_lb. iSplit.
+        - iApply lft_incl_trans. iSplit; last done.
+          iApply lft_le_incl. by exists κ.
+        - iApply lft_le_incl. exists κ1. by apply (comm _). }
+      iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
+      iFrame. iIntros (q') "!#Htok".
+      iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
+      iMod ("Hupd" with "*Htok") as "Hupd'". iModIntro. iNext.
+      iMod "Hupd'" as "[H Htok]". iMod ("Hclose" with "Htok") as "$".
+      iApply (ty_shr_mono with "Hincl' H").
+  Qed.
 
   Lemma lft_incl_ty_incl_shared_borrow ty κ1 κ2 :
     ty_incl (κ1 ⊑ κ2) (&shr{κ2}ty) (&shr{κ1}ty).
diff --git a/theories/typing.v b/theories/typing.v
index a5db5e0919ec9661a826d7be28f33a3d31aac95e..fa9f0f246559700043281be22de36d3639daaa0d 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -129,23 +129,24 @@ Section typing.
   Qed.
 
   Lemma typed_newlft ρ:
-    typed_step ρ Newlft (λ _, ∃ α, [α]{1} ∗ α ∋ top)%P.
+    typed_step ρ Newlft (λ _, ∃ α, 1.[α] ∗ α ∋ top)%P.
   Proof.
-    iIntros (tid) "!#(_&_&$)". wp_value. iMod lft_begin as (α) "[?#?]". done.
-    iMod (lft_borrow_create with "[][]") as "[_?]". done. done.
-    2:by iExists α; iFrame. eauto.
+    iIntros (tid) "!#(_&_&$)". wp_value. iMod lft_create as (α) "[?#?]". done.
+    iExists α. iFrame. iApply fupd_mask_mono. done.
+    iMod (borrow_create with "[]") as "[_?]". reflexivity. 2:by iIntros "!>". eauto.
   Qed.
 
-  Lemma typed_endlft κ ρ:
-    typed_step (κ ∋ ρ ∗ [κ]{1}) Endlft (λ _, ρ)%P.
-  Proof.
-    iIntros (tid) "!#(_&[Hextr [Htok #Hlft]]&$)". wp_bind (#() ;; #())%E.
-    iApply (wp_wand_r _ _ (λ _, _ ∗ True)%I). iSplitR "Hextr".
-    iApply (wp_frame_step_l with "[-]"); try done.
-    iDestruct (lft_end with "Hlft Htok") as "$". by wp_seq.
-    iIntros (v) "[#Hκ _]". iMod (lft_extract_out with "Hκ Hextr"). done.
-    by wp_seq.
-  Qed.
+  (* TODO : lifetime ending permission. *)
+  (* Lemma typed_endlft κ ρ: *)
+  (*   typed_step (κ ∋ ρ ∗ 1.[κ]) Endlft (λ _, ρ)%P. *)
+  (* Proof. *)
+  (*   iIntros (tid) "!#(_&[Hextr Htok]&$)". wp_bind (#() ;; #())%E. *)
+  (*   iApply (wp_wand_r _ _ (λ _, _ ∗ True)%I). iSplitR "Hextr". *)
+  (*   iApply (wp_frame_step_l with "[-]"); try done. *)
+  (*   iDestruct (lft_end with "Hlft Htok") as "$". by wp_seq. *)
+  (*   iIntros (v) "[#Hκ _]". iMod (lft_extract_out with "Hκ Hextr"). done. *)
+  (*   by wp_seq. *)
+  (* Qed. *)
 
   Lemma typed_alloc ρ (n : nat):
     0 < n → typed_step_ty ρ (Alloc #n) (own 1 (uninit n)).
@@ -203,35 +204,33 @@ Section typing.
 
   Lemma consumes_copy_uniq_borrow ty κ κ' q:
     ty.(ty_dup) →
-    consumes ty (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P
-                (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
+    consumes ty (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
+                (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
-    iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & Htok & #Hκ') & Htl & HΦ)".
+    iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & Htok) & Htl & HΦ)".
     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_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
-    iMod (lft_borrow_open with "H↦ Htok") as "[H↦ Hclose']". set_solver.
+    iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
+    iMod (borrow_acc with "H↦ Htok") as "[H↦ Hclose']". set_solver.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
     iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
-    iMod (lft_borrow_close with "[H↦] Hclose'") as "[H↦ Htok]". set_solver.
-    { iExists _. by iFrame. }
+    iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]". by iExists _; iFrame.
     iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
   Qed.
 
   Lemma consumes_copy_shr_borrow ty κ κ' q:
     ty.(ty_dup) →
-    consumes ty (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P
-                (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
+    consumes ty (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
+                (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
-    iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & [Htok #Hκ']) & Htl & HΦ)".
+    iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & Htok) & Htl & HΦ)".
     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 %[=->].
-    iMod (lft_incl_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
+    iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
     rewrite (union_difference_L (nclose lrustN) ⊤); last done.
-    setoid_rewrite ->tl_own_union; try set_solver.
-    iDestruct "Htl" as "[Htl ?]".
+    setoid_rewrite ->tl_own_union; try set_solver. iDestruct "Htl" as "[Htl ?]".
     iMod (ty_shr_acc with "Hshr [$Htok $Htl]") as (q'') "[H↦ Hclose']"; try set_solver.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
@@ -253,38 +252,36 @@ Section typing.
   Qed.
 
   Lemma typed_deref_uniq_borrow_own ty ν κ κ' q q':
-    typed_step (ν ◁ &uniq{κ} own q' ty ∗ κ' ⊑ κ ∗ [κ']{q})
+    typed_step (ν ◁ &uniq{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
                (!ν)
-               (λ v, v ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
+               (λ v, v ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
-    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & $)". wp_bind ν.
+    iIntros (tid) "!#(#HEAP & (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_trade with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
-    iMod (lft_borrow_open with "H↦ Htok") as "[H↦ Hclose']". done.
+    iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
+    iMod (borrow_acc_strong with "H↦ Htok") as "[H↦ Hclose']". done.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & H† & Hown)".
     subst. rewrite heap_mapsto_vec_singleton. wp_read.
-    iMod (lft_borrow_close_stronger with "[H↦ H† Hown] Hclose' []") as "[Hbor Htok]";
-      first done; first 2 last.
-    - iMod (lft_borrow_split with "Hbor") as "[_ Hbor]". done.
-      iMod (lft_borrow_split with "Hbor") as "[_ Hbor]". done.
+    iMod ("Hclose'" with "*[H↦ H† Hown]") as "[Hbor Htok]"; last first.
+    - iMod (borrow_split with "Hbor") as "[_ Hbor]". done.
+      iMod (borrow_split with "Hbor") as "[_ Hbor]". done.
       iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto.
-    - by iFrame "H↦ H†".
-    - iIntros "!>(?&?&?)!>". iNext. iExists _.
+    - iIntros "{$H↦ $H† $Hown}!>[_(?&?&?)]!>". iNext. iExists _.
       rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
   Qed.
 
   Lemma typed_deref_shr_borrow_own ty ν κ κ' q q':
-    typed_step (ν ◁ &shr{κ} own q' ty ∗ κ' ⊑ κ ∗ [κ']{q})
+    typed_step (ν ◁ &shr{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
                (!ν)
-               (λ v, v ◁ &shr{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
+               (λ v, v ◁ &shr{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
-    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & $)". wp_bind ν.
+    iIntros (tid) "!#(#HEAP & (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_trade with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
+    iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
     iDestruct "H↦" as (vl) "[H↦b Hown]".
-    iMod (lft_frac_borrow_open with "[] H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
+    iMod (frac_borrow_acc with "[] H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
     { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
     iSpecialize ("Hown" $! _ with "Htok2").
     iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
@@ -299,49 +296,54 @@ Section typing.
   Qed.
 
   Lemma typed_deref_uniq_borrow_borrow ty ν κ κ' κ'' q:
-    typed_step (ν ◁ &uniq{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ [κ]{q} ∗ κ' ⊑ κ'')
+    typed_step (ν ◁ &uniq{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
                (!ν)
-               (λ v, v ◁ &uniq{κ'} ty ∗ κ ⊑ κ' ∗ [κ]{q})%P.
+               (λ v, v ◁ &uniq{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
   Proof.
-    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) & $)". wp_bind ν.
+    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & Htok & #H⊑2) & $)". 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_trade with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
-    iMod (lft_borrow_exists with "H↦ Htok") as (vl) "[Hbor Htok]". done.
-    iMod (lft_borrow_split with "Hbor") as "[H↦ Hbor]". done.
-    iMod (lft_borrow_exists with "Hbor Htok") as (l') "[Hbor Htok]". done.
-    iMod (lft_borrow_split with "Hbor") as "[Heq Hbor]". done.
-    iMod (lft_borrow_persistent with "Heq Htok") as "[>% [Htok1 Htok2]]". done. subst.
-    iMod (lft_borrow_open with "H↦ Htok1") as "[>H↦ Hclose']". done.
-    iMod (lft_borrow_open with "Hbor Htok2") as "[Hbor Hclose'']". done.
+    iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
+    iMod (borrow_exists with "H↦ Htok") as (vl) "[Hbor Htok]". done.
+    iMod (borrow_split with "Hbor") as "[H↦ Hbor]". done.
+    iMod (borrow_exists with "Hbor Htok") as (l') "[Hbor Htok]". done.
+    iMod (borrow_split with "Hbor") as "[Heq Hbor]". done.
+    iMod (borrow_unnest with "Hbor") as "Hbor". done.
+    iMod (borrow_persistent with "Heq Htok") as "[>% Htok]". done. subst.
+    iMod (borrow_acc with "H↦ Htok") as "[>H↦ Hclose']". done.
     rewrite heap_mapsto_vec_singleton. wp_read.
-    iMod (lft_borrow_close with "[$H↦] Hclose'") as "[_ Htok1]". done.
-    iMod (lft_borrow_unnest with "H⊑2 [$Hbor $Hclose'']") as "[Htok2 Hbor]". done.
-    iMod ("Hclose" with "[$Htok1 $Htok2]") as "$".
-    iFrame "#". iExists _. eauto.
+    iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
+    iMod ("Hclose" with "Htok") as "$". iFrame "#".
+    iMod "Hbor". iExists _. iSplitR. done. iApply (borrow_shorten with "[] Hbor").
+    iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl.
   Qed.
 
   Lemma typed_deref_shr_borrow_borrow ty ν κ κ' κ'' q:
-    typed_step (ν ◁ &shr{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ [κ]{q} ∗ κ' ⊑ κ'')
+    typed_step (ν ◁ &shr{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
                (!ν)
-               (λ v, v ◁ &shr{κ'} ty ∗ κ ⊑ κ' ∗ [κ]{q})%P.
+               (λ v, v ◁ &shr{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
   Proof.
-    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) & $)". wp_bind ν.
+    iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & Htok & #H⊑2) & $)". 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 Hshr]".
     iDestruct "Heq" as %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
-    iMod (lft_incl_trade with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
-    iMod (lft_frac_borrow_open with "[] H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
+    iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
+    iMod (frac_borrow_acc with "[] H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
     { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
-    iSpecialize ("Hown" $! _ _ with "[$H⊑2 $Htok2]"). iApply lft_incl_refl.
-    iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
+    iAssert (κ' ⊑ κ'' ⋅ κ') as "#H⊑3".
+    { iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
+    iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
+    iSpecialize ("Hown" $! _ with "Htok").
+    iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose' Hclose''"; last first.
     - iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q''} v ∗ v = #l')%I); try done.
       iSplitL "Hown"; last by wp_read; eauto.
       iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ heapN);
         last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
     - iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
+      iMod ("Hclose''" with "Htok") as "Htok".
       iMod ("Hclose'" with "[$H↦]") as "Htok'".
-      iMod ("Hclose" with "[$Htok $Htok']") as "$". iFrame "#". iExists _. eauto.
+      iMod ("Hclose" with "[$Htok $Htok']") as "$". iFrame "#". iExists _.
+      iSplitL. done. iApply (ty_shr_mono with "H⊑3 Hshr").
   Qed.
 
   Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
@@ -367,18 +369,17 @@ Section typing.
   Qed.
 
   Lemma update_weak ty q κ κ':
-    update ty (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P
-              (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
+    update ty (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
+              (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
-    iIntros (ν tid Φ E ?) "[(H◁ & #H⊑ & Htok & #Hκ) HΦ]".
+    iIntros (ν tid Φ E ?) "[(H◁ & #H⊑ & Htok) HΦ]".
     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_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
-    iMod (lft_borrow_open with "H↦ Htok") as "[H↦ Hclose']". set_solver.
+    iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
+    iMod (borrow_acc with "H↦ Htok") as "[H↦ Hclose']". set_solver.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
     iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%#". iIntros (vl') "[H↦ Hown]".
-    iMod (lft_borrow_close with "[H↦ Hown] Hclose'") as "[Hbor Htok]". set_solver.
-    { iExists _. iFrame. }
+    iMod ("Hclose'" with "[H↦ Hown]") as "[Hbor Htok]". by iExists _; iFrame.
     iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
   Qed.
 
@@ -403,7 +404,7 @@ Section typing.
     iIntros (l vl) "(% & % & H↦ & Hupd)". wp_bind ν2.
     iApply (Hcons with "[- $H2 $Htl]"). done.
     iIntros (l' vl' q) "(% & % & H↦' & Hcons)". iApply wp_fupd.
-    iMod "Hcons". iApply wp_memcpy; last iFrame "∗#"; try done. iNext.
+    iMod "Hcons". iApply (wp_memcpy with "[$HEAP $H↦' $H↦]"); try done. iNext.
     iIntros "[H↦ H↦']". iMod "Hcons" as "[Hown' Hcons]".
     iMod ("Hcons" with "H↦'") as "[$$]". iApply "Hupd". by iFrame.
   Qed.