diff --git a/_CoqProject b/_CoqProject
index c4ae5b38be5032c7027833b1b1003f4740daa6b4..cd1cc58d5d66157d2121e98226ff5d33efe52bf4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -12,6 +12,9 @@ theories/races.v
 theories/tactics.v
 theories/wp_tactics.v
 theories/lifetime.v
+theories/tl_borrow.v
+theories/shr_borrow.v
+theories/frac_borrow.v
 theories/type.v
 theories/type_incl.v
 theories/perm.v
diff --git a/theories/frac_borrow.v b/theories/frac_borrow.v
new file mode 100644
index 0000000000000000000000000000000000000000..fa85e2aa562f5c0e3a270cea2fa57e029dc6ba32
--- /dev/null
+++ b/theories/frac_borrow.v
@@ -0,0 +1,120 @@
+From Coq Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import frac.
+From lrust Require Export lifetime shr_borrow.
+
+Class frac_borrowG Σ := frac_borrowG_inG :> inG Σ fracR.
+
+Definition frac_borrow `{invG Σ, lifetimeG Σ, frac_borrowG Σ} κ (Φ : Qp → iProp Σ) :=
+  (∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗
+                       (q = 1%Qp ∨ ∃ q', (q + q')%Qp = 1%Qp ∗ q'.[κ']))%I.
+Notation "&frac{ κ } P" := (frac_borrow κ P)
+  (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
+
+Section frac_borrow.
+
+  Context `{invG Σ, lifetimeG Σ, frac_borrowG Σ}.
+
+  Global Instance frac_borrow_proper :
+    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_borrow κ).
+  Proof. solve_proper. Qed.
+  Global Instance frac_borrow_persistent : PersistentP (&frac{κ}φ) := _.
+
+  Lemma borrow_fracture φ `(nclose lftN ⊆ E) κ:
+    &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
+  Proof.
+    iIntros "Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
+    iMod (borrow_acc_atomic_strong with "Hφ") as "[[Hφ Hclose]|[H† Hclose]]". done.
+    - iMod ("Hclose" with "*[-]") as "Hφ"; last first.
+      { 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 "[]".
+    - iMod ("Hclose" with "*") as "Hφ"; last first.
+      iExists γ, κ. iSplitR. by iApply lft_incl_refl.
+      iMod (borrow_fake with "H†"). done. by iApply borrow_share.
+  Qed.
+
+  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 frac_borrow.
+    iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
+    iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] 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.
+    iAssert (▷ φ qq ∗ ▷ φ (qφ0 + qφ / 2))%Qp%I with "[Hφqφ]" as "[$ Hqφ]".
+    { iNext. rewrite -{1}(Qp_div_2 qφ) {1}Hqφ. iApply "Hφ". by rewrite assoc. }
+    rewrite -{1}(Qp_div_2 qφ) {1}Hqφ -assoc {1}Hqκ'.
+    iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]".
+    iMod ("Hclose'" with "[Hqφ Hq Hown Hκq]") as "Hκ1".
+    { iNext. iExists _. iFrame. iRight. iDestruct "Hq" as "[%|Hq]".
+      - subst. iExists qq. iIntros "{$Hκq}!%".
+        by rewrite (comm _ qφ0) -assoc (comm _ qφ0) -Hqφ Qp_div_2.
+      - iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp.
+        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 (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. }
+    iDestruct "Hq" as (q') "[Hqφq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown".
+    iDestruct (own_valid with "Hown") as %Hval. iDestruct "Hqφq'" as %Hqφq'.
+    assert (0 < q'-qq ∨ qq = q')%Qc as [Hq'q|<-].
+    { change (qφ + qq ≤ 1)%Qc in Hval. apply Qp_eq in Hqφq'. simpl in Hval, Hqφq'.
+      rewrite <-Hqφq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
+      destruct Hval as [Hval|Hval].
+      by left; apply ->Qclt_minus_iff. by right; apply Qp_eq, Qc_is_canon. }
+    - assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. }
+      iDestruct "Hq'κ" as "[Hq'qκ Hqκ]".
+      iMod ("Hclose'" with "[Hqφ Hφqφ Hown Hq'qκ]") as "Hqκ2".
+      { iNext. iExists (qφ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "Hφ"; iFrame.
+        iRight. iExists _. iIntros "{$Hq'qκ}!%".
+        revert Hqφq'. rewrite !Qp_eq. move=>/=<-. ring. }
+      iApply "Hclose". iFrame. rewrite Hqκ' !lft_own_frac_op. by iFrame.
+    - iMod ("Hclose'" with "[Hqφ Hφqφ Hown]") as "Hqκ2".
+      { iNext. iExists (qφ ⋅ qq)%Qp. iFrame. iSplitL. by iApply "Hφ"; iFrame. auto. }
+      iApply "Hclose". rewrite -{2}(Qp_div_2 qκ') {2}Hqκ' !lft_own_frac_op. by iFrame.
+  Qed.
+
+  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 frac_borrow.
diff --git a/theories/lifetime.v b/theories/lifetime.v
index f0a3d50b541342ff26dbf1521235fc09cc75d421..2956516d7d3a1ae5814d342cd616f12e39e1e6ee 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -1,8 +1,6 @@
-From iris.algebra Require Import csum auth frac.
+From iris.algebra Require Import csum auth frac gmap.
 From iris.base_logic.lib Require Export fancy_updates invariants namespaces.
-From iris.base_logic.lib Require Import thread_local.
 From iris.proofmode Require Import tactics.
-From Coq Require Import Qcanon.
 
 Definition lftN := nroot .@ "lft".
 
@@ -19,7 +17,6 @@ Definition borrow_tokUR : ucmraT :=
 Class lifetimeG Σ := LifetimeG {
   lft_tok_inG :> inG Σ lft_tokUR;
   borrow_tok_inG :> inG Σ borrow_tokUR;
-  frac_inG :> inG Σ fracR;
   lft_toks_name : gname;
   borrow_tok_name : gname
 }.
@@ -347,220 +344,3 @@ Section incl.
 End incl.
 
 Typeclasses Opaque lft_incl.
-
-(*** Derived notions  *)
-
-(** Shared borrows  *)
-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 `{invG Σ, lifetimeG Σ} (P : iProp Σ).
-
-  Global Instance shr_borrow_proper :
-    Proper ((⊣⊢) ==> (⊣⊢)) (shr_borrow κ).
-  Proof. solve_proper. Qed.
-  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 shr_borrow_acc `(nclose lftN ⊆ E) κ :
-    &shr{κ}P ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ True) ∨
-                          [†κ] ∗ |={E∖lftN,E}=> True.
-  Proof.
-    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 shr_borrow_acc_tok `(nclose lftN ⊆ E) q κ :
-    &shr{κ}P ⊢ q.[κ] ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ q.[κ]).
-  Proof.
-    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 shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -∗ &shr{κ}P.
-  Proof.
-    iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
-      by iApply (idx_borrow_shorten with "H⊑").
-  Qed.
-
-End shared_borrows.
-
-Typeclasses Opaque shr_borrow.
-
-(** Fractured borrows  *)
-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" := (frac_borrow κ P)
-  (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
-
-Section frac_borrow.
-
-  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 borrow_fracture φ `(nclose lftN ⊆ E) κ:
-    &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
-  Proof.
-    iIntros "Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
-    iMod (borrow_acc_atomic_strong with "Hφ") as "[[Hφ Hclose]|[H† Hclose]]". done.
-    - iMod ("Hclose" with "*[-]") as "Hφ"; last first.
-      { 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 "[]".
-    - iMod ("Hclose" with "*") as "Hφ"; last first.
-      iExists γ, κ. iSplitR. by iApply lft_incl_refl.
-      iMod (borrow_fake with "H†"). done. by iApply borrow_share.
-  Qed.
-
-  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 frac_borrow.
-    iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
-    iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] 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.
-    iAssert (▷ φ qq ∗ ▷ φ (qφ0 + qφ / 2))%Qp%I with "[Hφqφ]" as "[$ Hqφ]".
-    { iNext. rewrite -{1}(Qp_div_2 qφ) {1}Hqφ. iApply "Hφ". by rewrite assoc. }
-    rewrite -{1}(Qp_div_2 qφ) {1}Hqφ -assoc {1}Hqκ'.
-    iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]".
-    iMod ("Hclose'" with "[Hqφ Hq Hown Hκq]") as "Hκ1".
-    { iNext. iExists _. iFrame. iRight. iDestruct "Hq" as "[%|Hq]".
-      - subst. iExists qq. iIntros "{$Hκq}!%".
-        by rewrite (comm _ qφ0) -assoc (comm _ qφ0) -Hqφ Qp_div_2.
-      - iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp.
-        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 (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. }
-    iDestruct "Hq" as (q') "[Hqφq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown".
-    iDestruct (own_valid with "Hown") as %Hval. iDestruct "Hqφq'" as %Hqφq'.
-    assert (0 < q'-qq ∨ qq = q')%Qc as [Hq'q|<-].
-    { change (qφ + qq ≤ 1)%Qc in Hval. apply Qp_eq in Hqφq'. simpl in Hval, Hqφq'.
-      rewrite <-Hqφq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
-      destruct Hval as [Hval|Hval].
-      by left; apply ->Qclt_minus_iff. by right; apply Qp_eq, Qc_is_canon. }
-    - assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. }
-      iDestruct "Hq'κ" as "[Hq'qκ Hqκ]".
-      iMod ("Hclose'" with "[Hqφ Hφqφ Hown Hq'qκ]") as "Hqκ2".
-      { iNext. iExists (qφ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "Hφ"; iFrame.
-        iRight. iExists _. iIntros "{$Hq'qκ}!%".
-        revert Hqφq'. rewrite !Qp_eq. move=>/=<-. ring. }
-      iApply "Hclose". iFrame. rewrite Hqκ' !lft_own_frac_op. by iFrame.
-    - iMod ("Hclose'" with "[Hqφ Hφqφ Hown]") as "Hqκ2".
-      { iNext. iExists (qφ ⋅ qq)%Qp. iFrame. iSplitL. by iApply "Hφ"; iFrame. auto. }
-      iApply "Hclose". rewrite -{2}(Qp_div_2 qκ') {2}Hqκ' !lft_own_frac_op. by iFrame.
-  Qed.
-
-  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 frac_borrow.
-
-(** Thread local borrows  *)
-
-Definition tl_borrow `{invG Σ, lifetimeG Σ, thread_localG Σ}
-           (κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
-  (∃ i, idx_borrow κ i P ∗ tl_inv tid N (idx_borrow_own 1 i))%I.
-
-Notation "&tl{ κ | tid | N } P" := (tl_borrow κ tid N P)
-  (format "&tl{ κ | tid | N } P", at level 20, right associativity) : uPred_scope.
-
-Section tl_borrow.
-  Context `{invG Σ, lifetimeG Σ, thread_localG Σ}
-          (tid : thread_id) (N : namespace) (P : iProp Σ).
-
-  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 borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ|tid|N}P.
-  Proof.
-    iIntros "HP". unfold borrow. iDestruct "HP" as (i) "[#? Hown]".
-    iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
-  Qed.
-
-  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).
-  Proof.
-    iIntros (???) "#HP[Hκ Htlown]".
-    iDestruct "HP" as (i) "(#Hpers&#Hinv)".
-    iMod (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try 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 tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P.
-  Proof.
-    iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
-    iApply (idx_borrow_shorten with "Hκκ' H").
-  Qed.
-
-End tl_borrow.
-
-Typeclasses Opaque tl_borrow.
diff --git a/theories/perm.v b/theories/perm.v
index c6cc6caa36a3962f3fe484ca31ad6a476bc78aa6..e268dacdf8cabb6f12732909ad20ccad03105779 100644
--- a/theories/perm.v
+++ b/theories/perm.v
@@ -8,7 +8,7 @@ Module Perm.
 
 Section perm.
 
-  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+  Context `{iris_typeG Σ}.
 
   Fixpoint eval_expr (ν : expr) : option val :=
     match ν with
@@ -70,7 +70,7 @@ Infix "∗" := sep (at level 80, right associativity) : perm_scope.
 
 Section duplicable.
 
-  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+  Context `{iris_typeG Σ}.
 
   Class Duplicable (ρ : @perm Σ) :=
     duplicable_persistent tid : PersistentP (ρ tid).
@@ -93,7 +93,7 @@ End duplicable.
 
 Section has_type.
 
-  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+  Context `{iris_typeG Σ}.
 
   Lemma has_type_value (v : val) ty tid :
     (v ◁ ty)%P tid ⊣⊢ ty.(ty_own) tid [v].
diff --git a/theories/perm_incl.v b/theories/perm_incl.v
index 93de38c14250b758264aea1ac7a08c0b8b45ba77..cca2d892ba399fdc1f6933b9a4838a163c885eb8 100644
--- a/theories/perm_incl.v
+++ b/theories/perm_incl.v
@@ -6,7 +6,7 @@ Import Perm Types.
 
 Section defs.
 
-  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+  Context `{iris_typeG Σ}.
 
   (* Definitions *)
   Definition perm_incl (ρ1 ρ2 : perm) :=
@@ -29,7 +29,7 @@ Notation "(⇔)" := (equiv (A:=perm)) (only parsing) : C_scope.
 
 Section props.
 
-  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+  Context `{iris_typeG Σ}.
 
   (* Properties *)
   Global Instance perm_incl_preorder : PreOrder (⇒).
diff --git a/theories/shr_borrow.v b/theories/shr_borrow.v
new file mode 100644
index 0000000000000000000000000000000000000000..b586f64c693467f4f29cfcfb4cb3029263220a90
--- /dev/null
+++ b/theories/shr_borrow.v
@@ -0,0 +1,54 @@
+From iris.algebra Require Import gmap auth frac.
+From iris.proofmode Require Import tactics.
+From lrust Require Export lifetime.
+
+(** Shared borrows  *)
+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 `{invG Σ, lifetimeG Σ} (P : iProp Σ).
+
+  Global Instance shr_borrow_proper :
+    Proper ((⊣⊢) ==> (⊣⊢)) (shr_borrow κ).
+  Proof. solve_proper. Qed.
+  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 shr_borrow_acc `(nclose lftN ⊆ E) κ :
+    &shr{κ}P ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ True) ∨
+                          [†κ] ∗ |={E∖lftN,E}=> True.
+  Proof.
+    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 shr_borrow_acc_tok `(nclose lftN ⊆ E) q κ :
+    &shr{κ}P ⊢ q.[κ] ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ q.[κ]).
+  Proof.
+    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 shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -∗ &shr{κ}P.
+  Proof.
+    iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
+      by iApply (idx_borrow_shorten with "H⊑").
+  Qed.
+
+End shared_borrows.
+
+Typeclasses Opaque shr_borrow.
diff --git a/theories/tl_borrow.v b/theories/tl_borrow.v
new file mode 100644
index 0000000000000000000000000000000000000000..41bfa9b520eca978621e2925e98466d018eb98b3
--- /dev/null
+++ b/theories/tl_borrow.v
@@ -0,0 +1,50 @@
+From lrust Require Export lifetime.
+From iris.base_logic.lib Require Export thread_local.
+From iris.proofmode Require Import tactics.
+
+Definition tl_borrow `{invG Σ, lifetimeG Σ, thread_localG Σ}
+           (κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
+  (∃ i, idx_borrow κ i P ∗ tl_inv tid N (idx_borrow_own 1 i))%I.
+
+Notation "&tl{ κ | tid | N } P" := (tl_borrow κ tid N P)
+  (format "&tl{ κ | tid | N } P", at level 20, right associativity) : uPred_scope.
+
+Section tl_borrow.
+  Context `{invG Σ, lifetimeG Σ, thread_localG Σ}
+          (tid : thread_id) (N : namespace) (P : iProp Σ).
+
+  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 borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ|tid|N}P.
+  Proof.
+    iIntros "HP". unfold borrow. iDestruct "HP" as (i) "[#? Hown]".
+    iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
+  Qed.
+
+  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).
+  Proof.
+    iIntros (???) "#HP[Hκ Htlown]".
+    iDestruct "HP" as (i) "(#Hpers&#Hinv)".
+    iMod (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try 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 tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P.
+  Proof.
+    iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
+    iApply (idx_borrow_shorten with "Hκκ' H").
+  Qed.
+
+End tl_borrow.
+
+Typeclasses Opaque tl_borrow.
diff --git a/theories/type.v b/theories/type.v
index be61b1d533d88a37039f94c2c18d65d6dc4c3452..46231d466240721d2a80b4a0690155e3c90bec5e 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -1,7 +1,14 @@
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Export thread_local.
 From iris.program_logic Require Import hoare.
-From lrust Require Export notation lifetime heap.
+From lrust Require Export notation lifetime frac_borrow heap.
+
+Class iris_typeG Σ := Iris_typeG {
+  type_heapG :> heapG Σ;
+  type_lifetimeG :> lifetimeG Σ;
+  type_thread_localG :> thread_localG Σ;
+  type_frac_borrowG Σ :> frac_borrowG Σ
+}.
 
 Definition mgmtE := nclose tlN ∪ lftN.
 Definition lrustN := nroot .@ "lrust".
@@ -9,12 +16,11 @@ Definition lrustN := nroot .@ "lrust".
 (* [perm] is defined here instead of perm.v in order to define [cont] *)
 Definition perm {Σ} := thread_id → iProp Σ.
 
-(* We would like to put the defintions of [type] and [simple_type] in
-   a section to generalize over [Σ] and all the [xxxG], but
-   [simple_type] would not depend on all that and this would make us
-   unable to define [ty_of_st] as a coercion... *)
+Section type.
+
+Context `{iris_typeG Σ}.
 
-Record type `{heapG Σ, lifetimeG Σ, thread_localG Σ} :=
+Record type :=
   { ty_size : nat; ty_dup : bool;
     ty_own : thread_id → list val → iProp Σ;
     ty_shr : lifetime → thread_id → namespace → loc → iProp Σ;
@@ -44,7 +50,10 @@ Record type `{heapG Σ, lifetimeG Σ, thread_localG Σ} :=
   }.
 Global Existing Instances ty_shr_persistent ty_dup_persistent.
 
-Record simple_type `{heapG Σ, lifetimeG Σ, thread_localG Σ} :=
+(* We are repeating the typeclass parameter here jsut to make sure
+   that simple_type does depend on it. Otherwise, the coercion defined
+   bellow will not be acceptable by Coq. *)
+Record simple_type `{iris_typeG Σ} :=
   { st_size : nat;
     st_own : thread_id → list val → iProp Σ;
 
@@ -52,8 +61,7 @@ Record simple_type `{heapG Σ, lifetimeG Σ, thread_localG Σ} :=
     st_own_persistent tid vl : PersistentP (st_own tid vl) }.
 Global Existing Instance st_own_persistent.
 
-Program Coercion ty_of_st `{heapG Σ, lifetimeG Σ, thread_localG Σ}
-        (st : simple_type) : type :=
+Program Coercion ty_of_st (st : simple_type) : type :=
   {| ty_size := st.(st_size); ty_dup := true;
      ty_own := st.(st_own);
 
@@ -65,7 +73,7 @@ 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".
+  intros st E N κ l tid q ? ?. iIntros "Hmt Htok".
   iMod (borrow_exists with "Hmt") as (vl) "Hmt". set_solver.
   iMod (borrow_split with "Hmt") as "[Hmt Hown]". set_solver.
   iMod (borrow_persistent with "Hown Htok") as "[Hown $]". set_solver.
@@ -74,12 +82,11 @@ Next Obligation.
   done. set_solver.
 Qed.
 Next Obligation.
-  intros Σ???. iIntros (st κ κ' tid N l) "#Hord H".
-  iDestruct "H" as (vl) "[Hf Hown]".
+  iIntros (st κ κ' tid N l) "#Hord H". iDestruct "H" as (vl) "[Hf Hown]".
   iExists vl. iFrame. by iApply (frac_borrow_shorten with "Hord").
 Qed.
 Next Obligation.
-  intros Σ??? st κ tid N E l q ??.  iIntros "#Hshr[Hlft $]".
+  intros st κ tid N E l q ??.  iIntros "#Hshr[Hlft $]".
   iDestruct "Hshr" as (vl) "[Hf Hown]".
   iMod (frac_borrow_acc with "[] Hf Hlft") as (q') "[Hmt Hclose]";
     first set_solver.
@@ -97,13 +104,15 @@ Next Obligation.
       iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
 Qed.
 
+End type.
+
 Delimit Scope lrust_type_scope with T.
 Bind Scope lrust_type_scope with type.
 
 Module Types.
 Section types.
 
-  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+  Context `{iris_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
diff --git a/theories/type_incl.v b/theories/type_incl.v
index 5366276b7f58c26d47bf22ec41e40726755c490c..2c8a0c1cbc1574170f0897302dfdb18d97f09ba1 100644
--- a/theories/type_incl.v
+++ b/theories/type_incl.v
@@ -6,7 +6,7 @@ Import Types.
 
 Section ty_incl.
 
-  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+  Context `{iris_typeG Σ}.
 
   Definition ty_incl (ρ : perm) (ty1 ty2 : type) :=
     ∀ tid, ρ tid ={⊤}=∗
diff --git a/theories/typing.v b/theories/typing.v
index b8249aa1221b75ccb064d0d6c7483bfb9fada68c..9e8d0a004d1a6ae86c864405efed48f8462e9a9a 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -6,7 +6,7 @@ Import Types Perm.
 
 Section typing.
 
-  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+  Context `{iris_typeG Σ}.
 
   (* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
   Definition typed_step (ρ : perm) e (θ : val → perm) :=
@@ -150,7 +150,7 @@ Section typing.
   Proof.
     iIntros (? tid) "!#(#HEAP&_&$)". wp_alloc l vl as "H↦" "H†". iIntros "!>".
     iExists _. iSplit. done. iNext. rewrite Nat2Z.id. iFrame.
-    apply (inj Z.of_nat) in H3. iExists _. iFrame. auto.
+    iExists _. iFrame. iPureIntro. by apply (inj Z.of_nat).
   Qed.
 
   Lemma typed_free ty (ν : expr):