diff --git a/lifetime.v b/lifetime.v
index af76d5aacf6cf1f799d66b4b72f63c8967d8f899..b5861c4b02191b8858bf1c4ea9b2c75c84dd24e7 100644
--- a/lifetime.v
+++ b/lifetime.v
@@ -1,3 +1,4 @@
+From iris.algebra Require Import upred_big_op.
 From iris.program_logic Require Export viewshifts pviewshifts.
 From iris.program_logic Require Import invariants namespaces thread_local.
 From iris.prelude Require Import strings.
@@ -60,12 +61,25 @@ Section lft.
   Axiom lft_incl_persistent : ∀ κ κ', PersistentP (κ ⊑ κ').
   Global Existing Instance lft_incl_persistent.
 
+  Axiom lft_extract_proper : ∀ κ, Proper ((⊣⊢) ==> (⊣⊢)) (lft_extract κ).
+  Global Existing Instance lft_extract_proper.
+
+  Axiom lft_borrow_proper : ∀ κ, Proper ((⊣⊢) ==> (⊣⊢)) (lft_borrow κ).
+  Global Existing Instance lft_borrow_proper.
+
+  Axiom lft_open_borrow_proper :
+    ∀ κ q, Proper ((⊣⊢) ==> (⊣⊢)) (lft_open_borrow κ q).
+  Global Existing Instance lft_open_borrow_proper.
+
   Axiom lft_frac_borrow_persistent : ∀ κ P, PersistentP (lft_frac_borrow κ P).
   Global Existing Instance lft_frac_borrow_persistent.
 
   Axiom lft_pers_borrow_persistent :
     ∀ κ i P, PersistentP (lft_pers_borrow κ i P).
   Global Existing Instance lft_pers_borrow_persistent.
+  Axiom lft_pers_borrow_proper :
+    ∀ κ i, Proper ((⊣⊢) ==> (⊣⊢)) (lft_pers_borrow κ i).
+  Global Existing Instance lft_pers_borrow_proper.
 
   Axiom lft_pers_borrow_own_timeless :
     ∀ i κ, TimelessP (lft_pers_borrow_own i κ).
@@ -92,7 +106,7 @@ Section lft.
       ▷ P ★ lft_open_borrow κ q P ={E}=> &{κ}P ★ [κ]{q}.
   Axiom lft_open_borrow_contravar :
     ∀ `(nclose lftN ⊆ E) κ P Q q,
-      ▷ (▷Q ={⊤ ∖ nclose lftN}=★ ▷P) ★ lft_open_borrow κ q P
+      lft_open_borrow κ q P ★ ▷ (▷Q ={⊤ ∖ nclose lftN}=★ ▷P)
       ={E}=> lft_open_borrow κ q Q.
   Axiom lft_reborrow :
     ∀ `(nclose lftN ⊆ E) κ κ' P, κ' ⊑ κ ⊢ &{κ}P ={E}=> &{κ'}P ★ κ' ∋ &{κ}P.
@@ -139,6 +153,13 @@ Section lft.
 
   (*** Derived lemmas  *)
 
+  Lemma lft_own_split κ q : [κ]{q} ⊣⊢ ([κ]{q/2} ★ [κ]{q/2}).
+  Proof. by rewrite lft_own_op Qp_div_2. Qed.
+
+  Global Instance into_and_lft_own κ q :
+    IntoAnd false ([κ]{q}) ([κ]{q/2}) ([κ]{q/2}).
+  Proof. by rewrite /IntoAnd lft_own_split. Qed.
+
   Lemma lft_borrow_open' E κ P q :
     nclose lftN ⊆ E →
       &{κ}P ★ [κ]{q} ={E}=> ▷ P ★ (▷ P ={E}=★ &{κ}P ★ [κ]{q}).
@@ -157,6 +178,24 @@ Section lft.
     iFrame. by iApply (lft_mkincl with "Hκ [-]").
   Qed.
 
+  Lemma lft_borrow_close_stronger `(nclose lftN ⊆ E) κ P Q q :
+    ▷ Q ★ lft_open_borrow κ q P ★ ▷ (▷Q ={⊤ ∖ nclose lftN}=★ ▷P)
+      ={E}=> &{κ}Q ★ [κ]{q}.
+  Proof.
+    iIntros "[HP Hvsob]".
+    iVs (lft_open_borrow_contravar with "Hvsob"). set_solver.
+    iApply (lft_borrow_close with "[-]"). set_solver. by iSplitL "HP".
+  Qed.
+
+  Lemma lft_borrow_big_sepL_split `(nclose lftN ⊆ E) {A} κ Φ (l : list A) :
+    &{κ}([★ list] k↦y ∈ l, Φ k y) ={E}=> [★ list] k↦y ∈ l, &{κ}(Φ k y).
+  Proof.
+    revert Φ. induction l=>Φ; iIntros. by rewrite !big_sepL_nil.
+    rewrite !big_sepL_cons.
+    iVs (lft_borrow_split with "[-]") as "[??]"; try done.
+    iFrame. by iVs (IHl with "[-]").
+  Qed.
+
 End lft.
 
 (*** Derived notions  *)
@@ -174,8 +213,10 @@ Section shared_borrows.
   Context `{irisG Λ Σ, lifetimeG Σ}
           (κ : lifetime) (N : namespace) (P : iProp Σ).
 
-  Instance lft_shr_borrow_persistent :
-    PersistentP (&shr{κ | N} P) := _.
+  Global Instance lft_shr_borrow_proper :
+    Proper ((⊣⊢) ==> (⊣⊢)) (lft_shr_borrow κ N).
+  Proof. solve_proper. Qed.
+  Global Instance lft_shr_borrow_persistent : PersistentP (&shr{κ | N} P) := _.
 
   Lemma lft_borrow_share E :
     lftN ⊥ N → &{κ}P ={E}=> &shr{κ|N}P.
@@ -229,8 +270,13 @@ Section tl_borrows.
   Context `{irisG Λ Σ, lifetimeG Σ, thread_localG Σ}
           (κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ).
 
-  Instance lft_tl_borrow_persistent :
-    PersistentP (&tl{κ|tid|N} P) := _.
+  Global Instance lft_tl_borrow_persistent : PersistentP (&tl{κ|tid|N} P) := _.
+  Global Instance lft_tl_borrow_proper :
+    Proper ((⊣⊢) ==> (⊣⊢)) (lft_tl_borrow κ tid N).
+  Proof.
+    intros P1 P2 EQ. apply uPred.exist_proper. intros κ'.
+    apply uPred.exist_proper. intros i. by rewrite EQ.
+  Qed.
 
   Lemma lft_borrow_share_tl E :
     lftN ⊥ N → &{κ}P ={E}=> &tl{κ|tid|N}P.
diff --git a/types.v b/types.v
index 45a32e169cc9a4d39b24c6c60243f34506a63ca5..c481893d1e3fb483b362d17b48ffeb52b9f0c86b 100644
--- a/types.v
+++ b/types.v
@@ -1,8 +1,11 @@
+From Coq Require Import Qcanon.
+From iris.algebra Require Import upred_big_op.
 From iris.program_logic Require Import thread_local.
 From lrust Require Export notation.
 From lrust Require Import lifetime heap.
 
 Definition mgmtE := nclose tlN ∪ lftN.
+Definition lrustN := nroot .@ "lrust".
 
 Section defs.
 
@@ -11,25 +14,32 @@ Section defs.
   Record type :=
     { ty_size : nat; ty_dup : bool;
       ty_own : thread_id → list val → iProp Σ;
-      ty_shr : lifetime → thread_id → coPset → loc → iProp Σ;
+      (* TODO : the document says ty_shr takes a mask, but it is never
+         used with anything else than namespaces. *)
+      ty_shr : lifetime → thread_id → namespace → loc → iProp Σ;
 
       ty_shr_persistent κ tid N l : PersistentP (ty_shr κ tid N l);
 
       ty_size_eq tid vl : ty_own tid vl ⊢ length vl = ty_size;
       ty_dup_dup tid vl : ty_dup → ty_own tid vl ⊢ ty_own tid vl ★ ty_own tid vl;
       (* The mask for starting the sharing does /not/ include the
-         namespace N, because sharing can be triggered in a context
-         where N is open. This should not be harmful, since sharing
-         typically creates invariants, which does not need the mask. *)
-      ty_share E N κ l tid q : nclose N ⊥ mgmtE → mgmtE ⊆ E →
+         namespace N, for allowing more flexibility for the user of
+         this type (typically for the [own] type). AFAIK, there is no
+         fundamental reason for this.
+
+         This should not be harmful, since sharing typically creates
+         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 ⊥ nclose N → mgmtE ⊆ E →
         &{κ} (l ↦★: ty_own tid) ★ [κ]{q} ={E}=> ty_shr κ tid N l ★ [κ]{q};
-      ty_shr_mono κ κ' tid E E' l : E ⊆ E' →
-        κ' ⊑ κ ⊢ ty_shr κ tid E l → ty_shr κ' tid E' l;
-      ty_shr_acc κ tid E E' l q :
-        E ⊆ E' → mgmtE ⊆ E' → ty_dup →
-        ty_shr κ tid E l ⊢
-          [κ]{q} ★ tl_own tid E ={E'}=> ∃ q', ▷l ↦★{q'}: ty_own tid ★
-             (▷l ↦★{q'}: ty_own tid ={E'}=★ [κ]{q} ★ tl_own tid E)
+      ty_shr_mono κ κ' tid N l :
+        κ' ⊑ κ ⊢ ty_shr κ tid N l → ty_shr κ' tid N l;
+      ty_shr_acc κ tid N E l q :
+        nclose N ⊆ E → mgmtE ⊆ E → ty_dup →
+        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)
     }.
 
   Global Existing Instance ty_shr_persistent.
@@ -58,10 +68,10 @@ Section defs.
     iVs (lft_borrow_fracture with "[Hmt]"); last by iFrame. done.
   Qed.
   Next Obligation.
-    iIntros (st κ κ' tid E E' l _) "#Hord". by iApply lft_frac_borrow_incl.
+    iIntros (st κ κ' tid N l) "#Hord". by iApply lft_frac_borrow_incl.
   Qed.
   Next Obligation.
-    intros st κ tid E E' l q ???.  iIntros "#Hshr!#[Hlft Htlown]".
+    intros st κ tid N E l q ???.  iIntros "#Hshr!#[Hlft Htlown]".
     iVs (lft_frac_borrow_open with "[] Hlft"); first set_solver; last by iFrame.
     iSplit; last done. iIntros "!#". iIntros (q1 q2). iSplit; iIntros "H".
     - iDestruct "H" as (vl) "[Hq1q2 Hown]".
@@ -86,28 +96,28 @@ Section types.
 
   Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
 
-  Program Definition bot : type :=
+  Program Definition bot :=
     ty_of_st {| st_size := 1; st_dup := true;
        st_own tid vl := False%I
     |}.
   Next Obligation. iIntros (tid vl) "[]". Qed.
   Next Obligation. iIntros (tid vl _) "[]". Qed.
 
-  Program Definition unit : type :=
+  Program Definition unit :=
     ty_of_st {| st_size := 0;  st_dup := true;
        st_own tid vl := (vl = [])%I
     |}.
   Next Obligation. iIntros (tid vl) "%". by subst. Qed.
   Next Obligation. iIntros (tid vl _) "%". auto. Qed.
 
-  Program Definition bool : type :=
+  Program Definition bool :=
     ty_of_st {| st_size := 1; st_dup := true;
        st_own tid vl := (∃ z:bool, vl = [ #z ])%I
     |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
   Next Obligation. iIntros (tid vl _) "H". auto. Qed.
 
-  Program Definition int : type :=
+  Program Definition int :=
     ty_of_st {| st_size := 1; st_dup := true;
        st_own tid vl := (∃ z:Z, vl = [ #z ])%I
     |}.
@@ -116,14 +126,14 @@ Section types.
 
   (* TODO own and uniq_borrow are very similar. They could probably
      somehow share some bits..  *)
-  Program Definition own (q:Qp) (ty:type) :=
+  Program Definition own (q : Qp) (ty : type) :=
     {| ty_size := 1; ty_dup := false;
        ty_own tid vl :=
          (∃ l:loc, vl = [ #l ] ★ †{q}l…ty.(ty_size)
                                  ★ ▷ l ↦★: ty.(ty_own) tid)%I;
-       ty_shr κ tid E l :=
+       ty_shr κ tid N l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ★
-            ∀ q', □ ([κ]{q'} →|={E ∪ mgmtE, mgmtE}▷=> ty.(ty_shr) κ tid E l' ★ [κ]{q'}))%I
+            ∀ q', □ ([κ]{q'} →|={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ tid N l' ★ [κ]{q'}))%I
     |}.
   Next Obligation.
     iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
@@ -133,46 +143,38 @@ Section types.
     intros q ty E N κ l tid q' ?? =>/=. iIntros "[Hshr Hq']".
     iVs (lft_borrow_open with "[Hshr Hq']") as "[Hown Hob]". set_solver. by iFrame.
     iDestruct "Hown" as (vl) "[Hmt Hvl]". iDestruct "Hvl" as (l') "(>%&Hf&Hown)". subst.
-    iVs (lft_open_borrow_contravar with "[Hob Hf]") as "Hob". set_solver.
-    { iSplitR "Hob"; last done. iIntros "!>[Hmt1 Hmt2]!==>!>". iExists [ #l' ].
-      rewrite heap_mapsto_vec_singleton. iSplitL "Hmt1"; first done.
-      iExists _. iSplit; [|by iSplitR "Hmt2"]. done. }
-    iVs (lft_borrow_close with "[Hmt Hown Hob]") as "[Hb Htok]". set_solver.
-    { rewrite heap_mapsto_vec_singleton. iSplitR "Hob"; last done.
-      by iIntros "!>{$Hmt$Hown}". }
+    iCombine "Hown" "Hmt" as "Hown". rewrite heap_mapsto_vec_singleton.
+    iVs (lft_borrow_close_stronger with "[-]") as "[Hb Htok]". set_solver.
+    { iIntros "{$Hown $Hob}!>[Hmt1 Hmt2]!==>!>". iExists [ #l'].
+      rewrite heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame. }
     iVs (lft_borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
-    iVs (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf".
-    rewrite lft_borrow_persist.
-    iDestruct "Hb2" as (κ0 i) "(#Hord&#Hpb&Hpbown)".
+    iVs (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb2") as "Hbf".
+    rewrite lft_borrow_persist. iDestruct "Hb1" as (κ0 i) "(#Hord&#Hpb&Hpbown)".
     iVs (inv_alloc N _ (lft_pers_borrow_own i κ0 ∨ ty_shr ty κ tid N l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
     iIntros "!==>{$Htok}". iExists l'. iFrame. iIntros (q'') "!#Htok".
-    iVs (inv_open with "Hinv") as "[[>Hbtok|#Hshr] Hclose]". set_solver.
-    - replace ((nclose N ∪ mgmtE) ∖ N) with mgmtE by set_solver.
-      iAssert (&{κ}▷ l' ↦★: ty_own ty tid)%I with "[Hbtok]" as "Hb".
+    iVs (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. }
       iVs (lft_borrow_open with "[Hb Htok]") as "[Hown Hob]". set_solver. by iFrame.
-      iVs (lft_open_borrow_contravar with "[Hob]") as "Hob". set_solver.
-      { iSplitR "Hob"; last done. instantiate (1:=(l' ↦★: ty_own ty tid)%I). eauto 10. }
       iIntros "!==>!>".
-      iVs (lft_borrow_close with "[Hown Hob]") as "[Hb Htok]". set_solver.
-        by iFrame "Hown".
-      iVs (ty.(ty_share) with "[Hb Htok]") as "[#Hshr Htok]"; try done. by iFrame.
+      iVs (lft_borrow_close_stronger with "[Hown Hob]") as "Hbtok". set_solver.
+      { iFrame "Hown Hob". eauto 10. }
+      iVs (ty.(ty_share) with "Hbtok") as "[#Hshr Htok]"; try done.
       iVs ("Hclose" with "[]") as "_"; by eauto.
-    - replace ((nclose N ∪ mgmtE) ∖ N) with mgmtE by set_solver.
-      iIntros "!==>!>". iVs ("Hclose" with "[]") as "_"; by eauto.
+    - iIntros "!==>!>". iVs ("Hclose" with "[]") as "_"; by eauto.
   Qed.
   Next Obligation.
-    intros _ ty κ κ' tid E E' l ?. iIntros "#Hκ #H".
-    iDestruct "H" as (l') "[Hfb Hvs]". iExists l'.
-    iSplit. by iApply (lft_frac_borrow_incl with "[]").
+    iIntros (_ ty κ κ' tid N l) "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]".
+    iExists l'. iSplit. by iApply (lft_frac_borrow_incl with "[]").
     iIntros (q') "!#Htok".
     iVs (lft_incl_trade with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
-    iApply (pvs_trans _ (E ∪ mgmtE)). iApply pvs_intro'. set_solver.
-    iIntros "Hclose'". iVs ("Hvs" $! q'' with "Htok") as "Hvs'".
-    iIntros "!==>!>". iVs "Hvs'" as "[Hshr Htok]". iVs "Hclose'".
+    iVs ("Hvs" $! q'' with "Htok") as "Hvs'".
+    iIntros "!==>!>". iVs "Hvs'" as "[Hshr Htok]".
     iVs ("Hclose" with "Htok"). iFrame.
-    iApply (ty.(ty_shr_mono) with "Hκ"); last done. done.
+    by iApply (ty.(ty_shr_mono) with "Hκ").
   Qed.
   Next Obligation. done. Qed.
 
@@ -180,10 +182,10 @@ Section types.
     {| ty_size := 1; ty_dup := false;
        ty_own tid vl :=
          (∃ l:loc, vl = [ #l ] ★ &{κ} l ↦★: ty.(ty_own) tid)%I;
-       ty_shr κ' tid E l :=
+       ty_shr κ' tid N l :=
          (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ★
             ∀ q' κ'', □ (κ'' ⊑ κ ★ κ'' ⊑ κ' ★ [κ'']{q'} →
-               |={E ∪ mgmtE, mgmtE}▷=> ty.(ty_shr) κ'' tid E l' ★ [κ'']{q'}))%I
+               |={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ'' tid N l' ★ [κ'']{q'}))%I
     |}.
   Next Obligation.
     iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
@@ -193,13 +195,10 @@ Section types.
     intros κ ty E N κ' l tid q' ?? =>/=. iIntros "[Hshr Hq']".
     iVs (lft_borrow_open with "[Hshr Hq']") as "[Hown Hob]". set_solver. by iFrame.
     iDestruct "Hown" as (vl) "[Hmt Hvl]". iDestruct "Hvl" as (l') "(>%&Hown)". subst.
-    iVs (lft_open_borrow_contravar with "[Hob]") as "Hob". set_solver.
-    { iSplitR "Hob"; last done. iIntros "!>[Hmt1 Hmt2]!==>!>". iExists [ #l' ].
-      rewrite heap_mapsto_vec_singleton. iSplitL "Hmt1"; first done.
-      iExists _. by iSplitR "Hmt2". }
-    iVs (lft_borrow_close with "[Hmt Hown Hob]") as "[Hb Htok]". set_solver.
-    { rewrite heap_mapsto_vec_singleton. iSplitR "Hob"; last done.
-      by iIntros "!>{$Hmt$Hown}". }
+    iCombine "Hmt" "Hown" as "Hown". rewrite heap_mapsto_vec_singleton.
+    iVs (lft_borrow_close_stronger with "[-]") as "[Hb Htok]". set_solver.
+    { iIntros "{$Hown $Hob}!>[Hmt1 Hmt2]!==>!>". iExists [ #l'].
+      rewrite heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame. }
     iVs (lft_borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
     iVs (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf".
     rewrite lft_borrow_persist.
@@ -208,9 +207,10 @@ Section types.
          with "[Hpbown]") as "#Hinv"; first by eauto.
     iIntros "!==>{$Htok}". iExists l'. iFrame.
     iIntros (q'' κ'') "!#(#Hκ''κ & #Hκ''κ' & Htok)".
-    iVs (inv_open with "Hinv") as "[[>Hbtok|#Hshr] Hclose]". set_solver.
-    - replace ((nclose N ∪ mgmtE) ∖ N) with mgmtE by set_solver.
-      iAssert (&{κ''}&{κ} l' ↦★: ty_own ty tid)%I with "[Hbtok]" as "Hb".
+    iVs (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. }
       iVs (lft_borrow_open with "[Hb Htok]") as "[Hown Hob]". set_solver. by iFrame.
@@ -226,26 +226,221 @@ Section types.
          need a lifetime that would be the union of κ and κ'. *)
       admit.
       by eauto.
-    - replace ((nclose N ∪ mgmtE) ∖ N) with mgmtE by set_solver.
-      iIntros "!==>!>". iVs ("Hclose" with "[]") as "_". by eauto.
+    - iIntros "!==>!>". iVs ("Hclose" with "[]") as "_". by eauto.
       iIntros "!==>{$Htok}". by iApply (ty.(ty_shr_mono) with "Hκ''κ'").
   Admitted.
   Next Obligation.
-    intros κ0 ty κ κ' tid E E' l ?. iIntros "#Hκ #H".
-    iDestruct "H" as (l') "[Hfb Hvs]". iExists l'.
-    iSplit. by iApply (lft_frac_borrow_incl with "[]").
+    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)".
-    iApply (pvs_trans _ (E ∪ mgmtE)). iApply pvs_intro'. set_solver.
-    iIntros "Hclose'". iVs ("Hvs" $! q' κ'' with "[Htok]") as "Hclose".
+    iVs ("Hvs" $! q' κ'' with "[Htok]") as "Hclose".
     { iFrame. iSplit. done. iApply lft_incl_trans. eauto. }
-    iIntros "!==>!>". iVs "Hclose" as "[Hshr Htok]". iVs "Hclose'".
-    iIntros "!==>{$Htok}". iApply (ty.(ty_shr_mono) with "[] Hshr"). done.
+    iIntros "!==>!>". iVs "Hclose" as "[Hshr Htok]".
+    iIntros "!==>{$Htok}". iApply (ty.(ty_shr_mono) with "[] Hshr").
     iApply lft_incl_refl.
   Qed.
   Next Obligation. done. Qed.
 
+  Program Definition shared_borrow (κ : lifetime) (ty : type) :=
+    ty_of_st {| st_size := 1; st_dup := true;
+      st_own tid vl := (∃ l:loc, vl = [ #l ] ★ ty.(ty_shr) κ tid lrustN l)%I
+    |}.
+  Next Obligation.
+    iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
+  Qed.
+  Next Obligation. iIntros (κ ty tid vl _) "H". auto. Qed.
+
+  Fixpoint combine_accu_size (tyl : list type) (accu : nat) :=
+    match tyl with
+    | [] => []
+    | ty :: q => (ty, accu) :: combine_accu_size q (accu + ty.(ty_size))
+    end.
 
+  Lemma list_ty_type_eq tid (tyl : list type) (vll : list (list val)) :
+    length tyl = length vll →
+    ([★ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))
+      ⊢ length (concat vll) = sum_list_with ty_size tyl.
+  Proof.
+    revert vll; induction tyl as [|ty tyq IH]; destruct vll;
+      iIntros (EQ) "Hown"; try done.
+    rewrite big_sepL_cons app_length /=. iDestruct "Hown" as "[Hown Hownq]".
+    iDestruct (ty.(ty_size_eq) with "Hown") as %->.
+    iDestruct (IH with "[-]") as %->; auto.
+  Qed.
+
+  Fixpoint nat_rec_shift {A : Type} (x : A) (f : nat → A → A) (n0 n : nat) :=
+    match n with
+    | O => x
+    | S n => f n0 (nat_rec_shift x f (S n0) n)
+    end.
+
+  Lemma split_prod_namespace tid (N : namespace) n :
+    ∃ E, (tl_own tid N ⊣⊢ tl_own tid E
+                 ★ nat_rec_shift True (λ i P, tl_own tid (N .@ i) ★ P) 0%nat n)
+         ∧ (∀ i, i < 0 → nclose (N .@ i) ⊆ E)%nat.
+  Proof.
+    generalize 0%nat. induction n as [|n IH].
+    - eexists. split. by rewrite right_id. intros. apply nclose_subseteq.
+    - intros i. destruct (IH (S i)) as [E [IH1 IH2]].
+      eexists (E ∖ (N .@ i))%I. split.
+      + simpl. rewrite IH1 assoc -tl_own_union; last set_solver.
+        f_equiv; last done. f_equiv. rewrite (comm union).
+        apply union_difference_L. apply IH2. lia.
+      + intros. assert (i0 ≠ i)%nat by lia. solve_ndisj.
+  Qed.
+
+  Program Definition product (tyl : list type) :=
+    {| ty_size := sum_list_with ty_size tyl; ty_dup := forallb ty_dup tyl;
+       ty_own tid vl :=
+         (∃ vll, vl = concat vll ★ length tyl = length vll ★
+                 [★ list] tyvl ∈ combine tyl vll, tyvl.1.(ty_own) tid (tyvl.2))%I;
+       ty_shr κ tid N l :=
+         ([★ list] i ↦ tyoffs ∈ combine_accu_size tyl 0,
+           tyoffs.1.(ty_shr) κ tid (N .@ i) (shift_loc l (tyoffs.2)))%I
+    |}.
+  Next Obligation.
+    iIntros (tyl tid vl) "Hown". iDestruct "Hown" as (vll) "(%&%&Hown)".
+    subst. by iApply (list_ty_type_eq with "Hown").
+  Qed.
+  Next Obligation.
+    induction tyl as [|ty tyq IH]; iIntros (tid vl Hfa) "H";
+      iDestruct "H" as ([|vl0 vlq]) "(%&#Hlen&Hown)"; subst vl;
+      iDestruct "Hlen" as %Hlen; inversion Hlen; simpl in *.
+    - iSplit; iExists []; by repeat iSplit.
+    - apply andb_prop_elim in Hfa. destruct Hfa as [Hfah Hfaq].
+      iDestruct (big_sepL_cons with "Hown") as "[Hh Hq]".
+      iDestruct (ty_dup_dup with "Hh") as "[Hh1 Hh2]". done.
+      iDestruct (IH tid (concat vlq) Hfaq with "[Hq]") as "[Hq1 Hq2]". by eauto.
+      iSplitL "Hh1 Hq1".
+      + iDestruct "Hq1" as (vllq) "(%&%&?)". iExists (vl0::vllq).
+        rewrite big_sepL_cons/=. iFrame. iSplit; iPureIntro; congruence.
+      + iDestruct "Hq2" as (vllq) "(%&%&?)". iExists (vl0::vllq).
+        rewrite big_sepL_cons/=. iFrame. iSplit; iPureIntro; congruence.
+  Qed.
+  Next Obligation.
+    intros tyl E N κ l tid q ??. iIntros "[Hown Htok]".
+    match goal with
+    | |- context [(&{κ}(?P))%I] =>
+      assert (P ⊣⊢ [★ list] i↦tyoffs ∈ combine_accu_size tyl 0,
+              (shift_loc l (tyoffs.2)) ↦★: ty_own (tyoffs.1) tid) as ->
+    end.
+    { rewrite -{1}(shift_loc_0 l). change 0%Z with (Z.of_nat 0).
+      generalize 0%nat. induction tyl as [|ty tyl IH]=>/= offs.
+      - iSplit; iIntros "_". by iApply big_sepL_nil.
+        iExists []. iSplit. by iApply heap_mapsto_vec_nil.
+        iExists []. repeat iSplit; try done. by iApply big_sepL_nil.
+      - rewrite big_sepL_cons -IH. iSplit.
+        + iIntros "H". iDestruct "H" as (vl) "[Hmt H]".
+          iDestruct "H" as ([|vl0 vll]) "(%&Hlen&Hown)";
+            iDestruct "Hlen" as %Hlen; inversion Hlen; subst.
+          rewrite big_sepL_cons heap_mapsto_vec_app/=.
+          iDestruct "Hmt" as "[Hmth Hmtq]"; iDestruct "Hown" as "[Hownh Hownq]".
+          iDestruct (ty.(ty_size_eq) with "#Hownh") as %->.
+          iSplitL "Hmth Hownh". iExists vl0. by iFrame.
+          iExists (concat vll). iSplitL "Hmtq"; last by eauto.
+          by rewrite shift_loc_assoc Nat2Z.inj_add.
+        + iIntros "[Hmth H]". iDestruct "H" as (vl) "[Hmtq H]".
+          iDestruct "H" as (vll) "(%&Hlen&Hownq)". subst.
+          iDestruct "Hmth" as (vlh) "[Hmth Hownh]". iDestruct "Hlen" as %->.
+          iExists (vlh ++ concat vll).
+          rewrite heap_mapsto_vec_app shift_loc_assoc Nat2Z.inj_add.
+          iDestruct (ty.(ty_size_eq) with "#Hownh") as %->. iFrame.
+          iExists (vlh :: vll). rewrite big_sepL_cons. iFrame. auto. }
+    iVs (lft_borrow_big_sepL_split with "Hown") as "Hown". set_solver.
+    (* FIXME : revert the (empty) proofmode context in the induction hypothesis. *)
+    iRevert "Htok Hown".
+    change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O at 3.
+    induction (combine_accu_size tyl 0) as [|[ty offs] ll IH].
+    - iIntros (?) "$ _ !==>". by rewrite big_sepL_nil.
+    - iIntros (i) "Htoks Hown". iDestruct (big_sepL_cons with "Hown") as "[Hownh Hownq]".
+      iVs (IH (S i)%nat with "[] Htoks Hownq") as "[#Hshrq Htoks]". done.
+      iVs (ty.(ty_share) _ (N .@ (i+0)%nat) with "[Hownh Htoks]") as "[#Hshrh $]".
+        solve_ndisj. done. by iFrame.
+      iVsIntro. rewrite big_sepL_cons. iFrame "#".
+      iApply big_sepL_mono; last done. intros. by rewrite /= Nat.add_succ_r.
+  Qed.
+  Next Obligation.
+    iIntros (tyl κ κ' tid N l) "#Hκ #H". iApply big_sepL_impl.
+    iSplit; last done. iIntros "!#*/=_#H'". by iApply (ty_shr_mono with "Hκ").
+  Qed.
+  Next Obligation.
+    intros tyl κ tid N E l q ?? DUP. simpl.
+    rewrite -{-1}(shift_loc_0 l). change 0%Z with (Z.of_nat 0). generalize 0%nat.
+    change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat).
+    destruct (split_prod_namespace tid N (length tyl)) as [Ef [EQ _]].
+    setoid_rewrite ->EQ. clear EQ. generalize 0%nat.
+    revert q. induction tyl as [|tyh tyq IH].
+    - iIntros (q i offs) "_!#$!==>". iExists 1%Qp. iSplitR; last by eauto.
+      iNext. iExists []. rewrite heap_mapsto_vec_nil. iSplit; first done.
+      simpl. iExists []. rewrite big_sepL_nil. eauto.
+    - simpl in DUP. destruct (andb_prop_elim _ _ DUP) as [DUPh DUPq]. simpl.
+      iIntros (q i offs) "#Hshr!#([Htokh Htokq]&Htlf&Htlh&Htlq)".
+      rewrite big_sepL_cons Nat.add_0_r.
+      iDestruct "Hshr" as "[Hshrh Hshrq]". setoid_rewrite <-Nat.add_succ_comm.
+      iVs (IH with "Hshrq [Htokq Htlf Htlq]") as (q'q) "[Hownq Hcloseq]". done. by iFrame.
+      iDestruct "Hownq" as (vlq) "[Hmtq Hownq]".
+      iDestruct "Hownq" as (vllq) "(>%&>%&Hownq)". subst vlq.
+      iDestruct (uPred.later_mono _ (_ = _) with "#Hownq") as ">Hlenvlq".
+        by apply list_ty_type_eq.
+      iDestruct "Hlenvlq" as %Hlenvlq.
+      iVs (tyh.(ty_shr_acc) with "Hshrh [Htokh Htlh]") as (q'h) "[Hownh Hcloseh]"; try done.
+      by pose proof (nclose_subseteq N i); set_solver. by iFrame.
+      iDestruct "Hownh" as (vlh) "[Hmth Hownh]".
+      iDestruct (uPred.later_mono _ (_ = _) with "#Hownh") as ">Hlenvlh". apply ty_size_eq.
+      iDestruct "Hlenvlh" as %Hlenvlh.
+      (** TODO : extract and simplify this arithmetic proof. *)
+      assert (∃ q' q'0h q'0q, q'h = q' + q'0h ∧ q'q = q' + q'0q)%Qp
+        as (q' & q'0h & q'0q & -> & ->).
+      { destruct (Qc_le_dec q'h q'q) as [LE0|LE0%Qclt_nge%Qclt_le_weak].
+        - destruct (q'q - q'h / 2)%Qp as [q'0q|] eqn:EQ; unfold Qp_minus in EQ;
+            destruct decide as [LT|LE%Qcnot_lt_le] in EQ; inversion EQ.
+          + exists (q'h / 2)%Qp, (q'h / 2)%Qp, q'0q. split; apply Qp_eq.
+            by rewrite Qp_div_2. subst; simpl; ring.
+          + apply (Qcplus_le_mono_r _ _ (-(q'h/2))%Qc) in LE0.
+            eapply Qcle_trans in LE; last apply LE0.
+            replace (q'h - q'h / 2)%Qc with (Qcmult q'h (1 - 1/2))%Qc in LE by ring.
+            replace 0%Qc with (Qcmult 0 (1-1/2)) in LE by ring.
+            by apply Qcmult_lt_0_le_reg_r, Qcle_not_lt in LE.
+        - destruct (q'h - q'q / 2)%Qp as [q'0h|] eqn:EQ; unfold Qp_minus in EQ;
+            destruct decide as [LT|LE%Qcnot_lt_le] in EQ; inversion EQ.
+          + exists (q'q / 2)%Qp, q'0h, (q'q / 2)%Qp. split; apply Qp_eq.
+            subst; simpl; ring. by rewrite Qp_div_2.
+          + apply (Qcplus_le_mono_r _ _ (-(q'q/2))%Qc) in LE0.
+            eapply Qcle_trans in LE; last apply LE0.
+            replace (q'q - q'q / 2)%Qc with (Qcmult q'q (1 - 1/2))%Qc in LE by ring.
+            replace 0%Qc with (Qcmult 0 (1-1/2)) in LE by ring.
+            by apply Qcmult_lt_0_le_reg_r, Qcle_not_lt in LE. }
+      iExists q'. iVsIntro. rewrite -!heap_mapsto_vec_op_eq.
+      iDestruct "Hmth" as "[Hmth0 Hmth1]". iDestruct "Hmtq" as "[Hmtq0 Hmtq1]".
+      iSplitR "Hcloseq Hcloseh Hmtq1 Hmth1".
+      + iNext. iExists (vlh ++ concat vllq). iDestruct (ty_size_eq with "#Hownh") as %Hlenh.
+        iSplitL "Hmtq0 Hmth0".
+        rewrite heap_mapsto_vec_app shift_loc_assoc Nat2Z.inj_add Hlenh; by iFrame.
+        iExists (vlh::vllq). iSplit. done. iSplit. iPureIntro; simpl; congruence.
+        rewrite big_sepL_cons. by iFrame.
+      + iIntros "H". iDestruct "H" as (vl) "[Hmt H]".
+        iDestruct "H" as ([|vllh' vllq']) "(>%&>%&Hown)". done. subst.
+        rewrite big_sepL_cons. iDestruct "Hown" as "[Hownh Hownq]".
+        iDestruct (uPred.later_mono _ (_ = _) with "#Hownq") as ">Hlenvlq'".
+          apply list_ty_type_eq; simpl in *; congruence.
+        iDestruct "Hlenvlq'" as %Hlenvlq'.
+        rewrite heap_mapsto_vec_app. iDestruct "Hmt" as "[Hmth0 Hmtq0]".
+        iCombine "Hmth0" "Hmth1" as "Hmth".
+        iDestruct (uPred.later_mono _ (_ = _) with "#Hownh") as ">Hlenvlh'".
+        apply ty_size_eq. iDestruct "Hlenvlh'" as %Hlenvlh'.
+        rewrite heap_mapsto_vec_op; last first. simpl in *; congruence.
+        iDestruct "Hmth" as "[>% Hmth]". subst.
+        iVs ("Hcloseh" with "[Hmth Hownh]") as "[Htokh $]".
+        { iNext. iExists _. by iFrame. }
+        iCombine "Hmtq0" "Hmtq1" as "Hmtq".
+        rewrite shift_loc_assoc Hlenvlh Nat2Z.inj_add heap_mapsto_vec_op; last congruence.
+        iDestruct "Hmtq" as "[>% Hmtq]".
+        iVs ("Hcloseq" with "[-Htokh]") as "[Htokq $]".
+        { iNext. iExists _. iFrame. iExists _. iFrame. iSplit. done.
+          simpl in *. iPureIntro. congruence. }
+        rewrite (lft_own_split _ q). by iFrame.
+  Qed.
 
 End types.
 
-End Types.
\ No newline at end of file
+End Types.