diff --git a/_CoqProject b/_CoqProject
index 2935afb5580998904c2319e797d469779b066d96..be0b3c395cd761abfa6678daf0db5a88b4ccd475 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -39,3 +39,4 @@ theories/typing/sum.v
 theories/typing/bool.v
 theories/typing/int.v
 theories/typing/function.v
+theories/typing/mem_instructions.v
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 31d8a7b8179b1e7dde248cbd5fa50c61f3e5f508..ea58722b29911eafa52f7923e725eac6b8ddf840 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -51,4 +51,4 @@ Section int.
     iIntros (v2) "[Hv2$]". iDestruct "Hv2" as (z2) "Hz2". iDestruct "Hz2" as %[=->].
     wp_op; intros _; by iExists _.
   Qed.
-End int.
\ No newline at end of file
+End int.
diff --git a/theories/typing/mem_instructions.v b/theories/typing/mem_instructions.v
new file mode 100644
index 0000000000000000000000000000000000000000..3e82fbb7b684881d4697c2757eaad0716a1b9f9b
--- /dev/null
+++ b/theories/typing/mem_instructions.v
@@ -0,0 +1,136 @@
+From Coq Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From lrust.lifetime Require Import borrow frac_borrow reborrow.
+From lrust.lang Require Export new_delete.
+From lrust.lang Require Import heap.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing product perm uninit own uniq_bor shr_bor.
+
+(** Typing rules for memory instructions. *)
+
+Section typing.
+  Context `{typeG Σ}.
+
+  Lemma typed_new ρ (n : nat):
+    0 ≤ n → typed_step_ty ρ (new [ #n]%E) (own n (uninit n)).
+  Proof.
+    iIntros (Hn tid) "!#(#HEAP&_&_&$)". iApply (wp_new with "HEAP"); try done.
+    iIntros "!>*(% & H† & H↦)". iExists _. iSplit. done. iNext.
+    rewrite Nat2Z.id. iSplitR "H†".
+    - iExists vl. iFrame.
+      match goal with H : Z.of_nat n = Z.of_nat (length vl) |- _ => rename H into Hlen end.
+      clear Hn. apply (inj Z.of_nat) in Hlen. subst.
+      iInduction vl as [|v vl] "IH". done.
+      iExists [v], vl. iSplit. done. by iSplit.
+    - by rewrite uninit_sz freeable_sz_full.
+  Qed.
+
+  Lemma typed_delete ty (ν : expr):
+    typed_step (ν ◁ own ty.(ty_size) ty) (delete [ #ty.(ty_size); ν])%E (λ _, top).
+  Proof.
+    iIntros (tid) "!#(#HEAP&_&H◁&$)". wp_bind ν.
+    iApply (has_type_wp with "[$H◁]"). iIntros (v) "_ H◁ !>".
+    rewrite has_type_value.
+    iDestruct "H◁" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
+    iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
+    rewrite ty_size_eq. iDestruct "Hown" as ">Hown". iDestruct "Hown" as %<-.
+    iApply (wp_delete with "[-]"); try by auto.
+    rewrite freeable_sz_full. by iFrame.
+  Qed.
+
+
+  Lemma typed_deref_uniq_bor_own ty ν κ κ' q q':
+    typed_step (ν ◁ &uniq{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
+               (!ν)
+               (λ v, v ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
+  Proof.
+    iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑ & Htok) & $)". wp_bind ν.
+    iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
+    rewrite has_type_value. iDestruct "H◁" as (l P) "[[Heq #HPiff] HP]".
+    iDestruct "Heq" as %[=->].
+    iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
+    iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
+    iMod (bor_acc_cons with "LFT H↦ Htok") as "[H↦ Hclose']". done.
+    iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & Hown & H†)".
+    subst. rewrite heap_mapsto_vec_singleton. wp_read.
+    iMod ("Hclose'" with "*[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
+    - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
+      iMod (bor_sep _ _ _ (l' ↦∗: ty_own ty tid) with "LFT Hbor") as "[_ Hbor]". done.
+      iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _, _.
+      iFrame. iSplitR. done. by rewrite -uPred.iff_refl.
+    - iFrame "H↦ H† Hown".
+    - iIntros "!>(?&?&?)!>". iNext. iExists _.
+      rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
+  Qed.
+
+  Lemma typed_deref_uniq_bor_bor ty ν κ κ' κ'' q:
+    typed_step (ν ◁ &uniq{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
+               (!ν)
+               (λ v, v ◁ &uniq{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
+  Proof.
+    iIntros (tid) "!#(#HEAP & #LFT & (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 P) "[[Heq #HPiff] HP]".
+    iDestruct "Heq" as %[=->].
+    iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
+    iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
+    iMod (bor_exists with "LFT H↦") as (vl) "Hbor". done.
+    iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
+    iMod (bor_exists with "LFT Hbor") as (l') "Hbor". done.
+    iMod (bor_exists with "LFT Hbor") as (P') "Hbor". done.
+    iMod (bor_sep with "LFT Hbor") as "[H Hbor]". done.
+    iMod (bor_persistent_tok with "LFT H Htok") as "[[>% #HP'iff] Htok]". done. subst.
+    iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
+    rewrite heap_mapsto_vec_singleton.
+    iApply (wp_fupd_step  _ (⊤∖↑lftN) with "[Hbor]"); try done.
+      by iApply (bor_unnest with "LFT Hbor").
+    wp_read. iIntros "!> Hbor". iFrame "#". iSplitL "Hbor".
+    - iExists _, _. iSplitR. by auto.
+      iApply (bor_shorten with "[] Hbor").
+      iApply (lft_incl_glb with "H⊑2"). iApply lft_incl_refl.
+    - iApply ("Hclose" with ">"). by iMod ("Hclose'" with "[$H↦]") as "[_ $]".
+  Qed.
+
+  Lemma typed_deref_shr_bor_own ty ν κ κ' q q':
+    typed_step (ν ◁ &shr{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
+               (!ν)
+               (λ v, v ◁ &shr{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
+  Proof.
+    iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑ & [Htok1 Htok2]) & $)". wp_bind ν.
+    iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
+    rewrite has_type_value. iDestruct "H◁" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
+    iMod (lft_incl_acc with "H⊑ Htok1") as (q'') "[Htok1 Hclose]". done.
+    iDestruct "H↦" as (vl) "[H↦b #Hown]".
+    iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
+    iMod (lft_incl_acc with "H⊑ Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
+    iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
+    - iApply ("Hown" with "* [%] Htok2"). set_solver+.
+    - wp_read. iIntros "!>[Hshr Htok2]{$H⊑}". iMod ("Hclose''" with "Htok2") as "$".
+      iSplitL "Hshr"; first by iExists _; auto. iApply ("Hclose" with ">").
+      iFrame. iApply "Hclose'". auto.
+  Qed.
+
+  Lemma typed_deref_shr_bor_bor ty ν κ κ' κ'' q:
+    typed_step (ν ◁ &shr{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
+               (!ν)
+               (λ v, v ◁ &shr{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
+  Proof.
+    iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑1 & [Htok1 Htok2] & #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_acc with "H⊑1 Htok1") as (q') "[Htok1 Hclose]". done.
+    iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
+    iAssert (κ' ⊑ κ'' ∪ κ')%I as "#H⊑3".
+    { iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
+    iMod (lft_incl_acc with "[] Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
+    { iApply (lft_incl_trans with "[]"); done. }
+    iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
+    - iApply ("Hown" with "* [%] Htok2"). set_solver+.
+    - wp_read. iIntros "!>[#Hshr Htok2]{$H⊑1}".
+      iMod ("Hclose''" with "Htok2") as "$". iSplitR.
+      * iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
+      * iApply ("Hclose" with ">"). iApply ("Hclose'" with "[$H↦]").
+  Qed.
+
+End typing.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 6c8ec1a2bea1054d9cfaed77ef855a56d454feec..b0ecdd9e449a0e44c38cb30b5eafa9f3e4df2042 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -1,10 +1,10 @@
 From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import big_op.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.lang Require Export new_delete.
-From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
-From lrust.typing Require Import typing product perm uninit.
+From lrust.typing Require Import perm typing uninit uniq_bor type_context.
 
 Section own.
   Context `{typeG Σ}.
@@ -116,32 +116,21 @@ Section own.
     Proper (eqtype E L ==> eqtype E L) (own n).
   Proof. intros ?? Heq. split; f_equiv; apply Heq. Qed.
 
-  Lemma typed_new ρ (n : nat):
-    0 ≤ n → typed_step_ty ρ (new [ #n]%E) (own n (uninit n)).
+  (** Typing *)
+  Lemma tctx_borrow E L p n ty κ :
+    tctx_incl E L [TCtx_hasty p (own n ty)]
+                  [TCtx_hasty p (&uniq{κ}ty); TCtx_blocked p κ (own n ty)].
   Proof.
-    iIntros (Hn tid) "!#(#HEAP&_&_&$)". iApply (wp_new with "HEAP"); try done.
-    iIntros "!>*(% & H† & H↦)". iExists _. iSplit. done. iNext.
-    rewrite Nat2Z.id. iSplitR "H†".
-    - iExists vl. iFrame.
-      match goal with H : Z.of_nat n = Z.of_nat (length vl) |- _ => rename H into Hlen end.
-      clear Hn. apply (inj Z.of_nat) in Hlen. subst.
-      iInduction vl as [|v vl] "IH". done.
-      iExists [v], vl. iSplit. done. by iSplit.
-    - by rewrite uninit_sz freeable_sz_full.
+    iIntros (tid ??) "#LFT $ $ H".
+    rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
+    iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l) "(EQ & Hmt & ?)".
+    iDestruct "EQ" as %[=->]. iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
+    iModIntro. iSplitL "Hbor".
+    - iExists _. iSplit. done. iExists _, _. erewrite <-uPred.iff_refl. eauto.
+    - iExists _. iSplit. done. iIntros "H†". iExists _. iFrame. iSplitR. by eauto.
+        by iMod ("Hext" with "H†") as "$".
   Qed.
 
-  Lemma typed_delete ty (ν : expr):
-    typed_step (ν ◁ own ty.(ty_size) ty) (delete [ #ty.(ty_size); ν])%E (λ _, top).
-  Proof.
-    iIntros (tid) "!#(#HEAP&_&H◁&$)". wp_bind ν.
-    iApply (has_type_wp with "[$H◁]"). iIntros (v) "_ H◁ !>".
-    rewrite has_type_value.
-    iDestruct "H◁" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
-    iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
-    rewrite ty_size_eq. iDestruct "Hown" as ">Hown". iDestruct "Hown" as %<-.
-    iApply (wp_delete with "[-]"); try by auto.
-    rewrite freeable_sz_full. by iFrame.
-  Qed.
 
   Lemma update_strong ty1 ty2 n:
     ty1.(ty_size) = ty2.(ty_size) →
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 2569da4fe34979835e0ebe3c6f81400704ba714b..73701ab9d775c8a481e9b1c973f47d60179e8b65 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -1,7 +1,6 @@
 From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import perm.
 
 Section product.
   Context `{typeG Σ}.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index ead69ede2ac4c70a4b7adc0177d23f17b0339a61..1b0fefad6b242f7372f3ca96d922e38831e1d75c 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -2,7 +2,7 @@ From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From lrust.lifetime Require Import frac_borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import perm lft_contexts type_context typing own uniq_bor.
+From lrust.typing Require Import perm lft_contexts type_context typing.
 
 Section shr_bor.
   Context `{typeG Σ}.
@@ -38,20 +38,6 @@ Notation "&shr{ κ } ty" := (shr_bor κ ty)
 Section typing.
   Context `{typeG Σ}.
 
-  Lemma tctx_incl_share E L p κ ty :
-    lctx_lft_alive E L κ → tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)] [TCtx_hasty p (&shr{κ}ty)].
-  Proof.
-    iIntros (Hκ ???) "#LFT HE HL Huniq".
-    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
-    rewrite /tctx_interp !big_sepL_singleton /=.
-    iDestruct "Huniq" as (v) "[% Huniq]". 
-    iDestruct "Huniq" as (l P) "[[% #HPiff] HP]".
-    iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
-    iMod (ty.(ty_share) with "LFT H↦ Htok") as "[Hown Htok]"; [solve_ndisj|].
-    iMod ("Hclose" with "Htok") as "[$ $]". iExists _. iFrame "%".
-    iIntros "!>/=". eauto.
-  Qed.
-
   Lemma tctx_reborrow_shr E L p ty κ κ' :
     lctx_lft_incl E L κ' κ →
     tctx_incl E L [TCtx_hasty p (&shr{κ}ty)]
@@ -90,46 +76,4 @@ Section typing.
     iMod ("Hclose'" with "[H↦]") as "[Htok $]". iExists _; by iFrame.
     iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
   Qed.
-
-  Lemma typed_deref_shr_bor_own ty ν κ κ' q q':
-    typed_step (ν ◁ &shr{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
-               (!ν)
-               (λ v, v ◁ &shr{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
-  Proof.
-    iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑ & [Htok1 Htok2]) & $)". wp_bind ν.
-    iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
-    rewrite has_type_value. iDestruct "H◁" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
-    iMod (lft_incl_acc with "H⊑ Htok1") as (q'') "[Htok1 Hclose]". done.
-    iDestruct "H↦" as (vl) "[H↦b #Hown]".
-    iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
-    iMod (lft_incl_acc with "H⊑ Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
-    iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
-    - iApply ("Hown" with "* [%] Htok2"). set_solver+.
-    - wp_read. iIntros "!>[Hshr Htok2]{$H⊑}". iMod ("Hclose''" with "Htok2") as "$".
-      iSplitL "Hshr"; first by iExists _; auto. iApply ("Hclose" with ">").
-      iFrame. iApply "Hclose'". auto.
-  Qed.
-
-  Lemma typed_deref_shr_bor_bor ty ν κ κ' κ'' q:
-    typed_step (ν ◁ &shr{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
-               (!ν)
-               (λ v, v ◁ &shr{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
-  Proof.
-    iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑1 & [Htok1 Htok2] & #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_acc with "H⊑1 Htok1") as (q') "[Htok1 Hclose]". done.
-    iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
-    iAssert (κ' ⊑ κ'' ∪ κ')%I as "#H⊑3".
-    { iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
-    iMod (lft_incl_acc with "[] Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
-    { iApply (lft_incl_trans with "[]"); done. }
-    iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
-    - iApply ("Hown" with "* [%] Htok2"). set_solver+.
-    - wp_read. iIntros "!>[#Hshr Htok2]{$H⊑1}".
-      iMod ("Hclose''" with "Htok2") as "$". iSplitR.
-      * iExists _. iSplitR. done. by iApply (ty_shr_mono with "LFT H⊑3 Hshr").
-      * iApply ("Hclose" with ">"). iApply ("Hclose'" with "[$H↦]").
-  Qed.
 End typing.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 6984b5c8ccde34e53197d4de25e1f801c287300a..3e78528ea3b335a906d28c652ffa56c82c43479d 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import fractional.
 From lrust.lifetime Require Import borrow frac_borrow.
-From lrust.typing Require Export type perm.
+From lrust.typing Require Export type.
 
 Section sum.
   Context `{typeG Σ}.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index c5fdfa53da2441702bf4f20200f5e24b788dbd6b..3544f3661a541bb4cc8ac039d9133d2c88e0182f 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -1,5 +1,5 @@
 From iris.base_logic.lib Require Export na_invariants.
-From lrust.lang Require Import heap.
+From lrust.lang Require Export proofmode notation.
 From lrust.lifetime Require Import borrow frac_borrow reborrow.
 From lrust.typing Require Import lft_contexts.
 
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index d588ff6729c1aab9dc5e52b0fc4d4b46394fdd97..a29d2cc2b0e41371cf7c594dd1f06aef389875eb 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -6,6 +6,8 @@ From lrust.typing Require Import perm lft_contexts type_context cont_context.
 From lrust.lang Require Import proofmode.
 From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
 
+(* TODO: Split this file into instructions.v and body.v. *)
+
 Section typing.
   Context `{typeG Σ}.
 
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 4d5551b2838f0a7be2d785bafa631adfb6020f0e..44cbc58469ccc29d416f8719f2fd9ac64b0d355d 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -3,7 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lifetime Require Import borrow reborrow frac_borrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
-From lrust.typing Require Import perm lft_contexts type_context typing own.
+From lrust.typing Require Import lft_contexts type_context shr_bor perm typing.
 
 Section uniq_bor.
   Context `{typeG Σ}.
@@ -106,18 +106,18 @@ Notation "&uniq{ κ } ty" := (uniq_bor κ ty)
 Section typing.
   Context `{typeG Σ}.
 
-  Lemma tctx_borrow E L p n ty κ :
-    tctx_incl E L [TCtx_hasty p (own n ty)]
-                  [TCtx_hasty p (&uniq{κ}ty); TCtx_blocked p κ (own n ty)].
+  Lemma tctx_incl_share E L p κ ty :
+    lctx_lft_alive E L κ → tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)] [TCtx_hasty p (&shr{κ}ty)].
   Proof.
-    iIntros (tid ??) "#LFT $ $ H".
-    rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
-    iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l) "(EQ & Hmt & ?)".
-    iDestruct "EQ" as %[=->]. iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
-    iModIntro. iSplitL "Hbor".
-    - iExists _. iSplit. done. iExists _, _. erewrite <-uPred.iff_refl. eauto.
-    - iExists _. iSplit. done. iIntros "H†". iExists _. iFrame. iSplitR. by eauto.
-        by iMod ("Hext" with "H†") as "$".
+    iIntros (Hκ ???) "#LFT HE HL Huniq".
+    iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
+    rewrite /tctx_interp !big_sepL_singleton /=.
+    iDestruct "Huniq" as (v) "[% Huniq]". 
+    iDestruct "Huniq" as (l P) "[[% #HPiff] HP]".
+    iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
+    iMod (ty.(ty_share) with "LFT H↦ Htok") as "[Hown Htok]"; [solve_ndisj|].
+    iMod ("Hclose" with "Htok") as "[$ $]". iExists _. iFrame "%".
+    iIntros "!>/=". eauto.
   Qed.
 
   Lemma tctx_reborrow_uniq E L p ty κ κ' :
@@ -159,58 +159,6 @@ Section typing.
     iExists _, _. erewrite <-uPred.iff_refl. auto.
   Qed.
 
-  Lemma typed_deref_uniq_bor_own ty ν κ κ' q q':
-    typed_step (ν ◁ &uniq{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
-               (!ν)
-               (λ v, v ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
-  Proof.
-    iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑ & Htok) & $)". wp_bind ν.
-    iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
-    rewrite has_type_value. iDestruct "H◁" as (l P) "[[Heq #HPiff] HP]".
-    iDestruct "Heq" as %[=->].
-    iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
-    iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
-    iMod (bor_acc_cons with "LFT H↦ Htok") as "[H↦ Hclose']". done.
-    iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & Hown & H†)".
-    subst. rewrite heap_mapsto_vec_singleton. wp_read.
-    iMod ("Hclose'" with "*[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
-    - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
-      iMod (bor_sep _ _ _ (l' ↦∗: ty_own ty tid) with "LFT Hbor") as "[_ Hbor]". done.
-      iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _, _.
-      iFrame. iSplitR. done. by rewrite -uPred.iff_refl.
-    - iFrame "H↦ H† Hown".
-    - iIntros "!>(?&?&?)!>". iNext. iExists _.
-      rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
-  Qed.
-
-  Lemma typed_deref_uniq_bor_bor ty ν κ κ' κ'' q:
-    typed_step (ν ◁ &uniq{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
-               (!ν)
-               (λ v, v ◁ &uniq{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
-  Proof.
-    iIntros (tid) "!#(#HEAP & #LFT & (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 P) "[[Heq #HPiff] HP]".
-    iDestruct "Heq" as %[=->].
-    iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
-    iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
-    iMod (bor_exists with "LFT H↦") as (vl) "Hbor". done.
-    iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
-    iMod (bor_exists with "LFT Hbor") as (l') "Hbor". done.
-    iMod (bor_exists with "LFT Hbor") as (P') "Hbor". done.
-    iMod (bor_sep with "LFT Hbor") as "[H Hbor]". done.
-    iMod (bor_persistent_tok with "LFT H Htok") as "[[>% #HP'iff] Htok]". done. subst.
-    iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
-    rewrite heap_mapsto_vec_singleton.
-    iApply (wp_fupd_step  _ (⊤∖↑lftN) with "[Hbor]"); try done.
-      by iApply (bor_unnest with "LFT Hbor").
-    wp_read. iIntros "!> Hbor". iFrame "#". iSplitL "Hbor".
-    - iExists _, _. iSplitR. by auto.
-      iApply (bor_shorten with "[] Hbor").
-      iApply (lft_incl_glb with "H⊑2"). iApply lft_incl_refl.
-    - iApply ("Hclose" with ">"). by iMod ("Hclose'" with "[$H↦]") as "[_ $]".
-  Qed.
-
   Lemma update_weak ty q κ κ':
     update ty (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
               (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.