diff --git a/_CoqProject b/_CoqProject
index 1dc5058dc9236159eb5ca1a5aaa77a83fc7f8e12..0e5f1183e8db25d3387be6c04a5c61430b8a770b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -40,5 +40,5 @@ theories/typing/bool.v
 theories/typing/int.v
 theories/typing/function.v
 theories/typing/programs.v
-theories/typing/mem.v
+theories/typing/borrow.v
 theories/typing/cont.v
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index b0fc52ebebd33deee34fef8936e3313cc098b121..0e5d6d58b6e32a4411c8f580c90e8894e5ea7682 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -11,6 +11,10 @@ Section bool.
 
   Global Instance bool_send : Send bool.
   Proof. iIntros (tid1 tid2 vl). done. Qed.
+End bool.
+
+Section typing.
+  Context `{typeG Σ}.
 
   Lemma type_bool (b : Datatypes.bool) E L :
     typed_instruction_ty E L [] #b bool.
@@ -26,10 +30,10 @@ Section bool.
     (* FIXME why can't I merge these two iIntros? *)
     iIntros (He1 He2). iIntros (tid qE) "#LFT HE HL HC".
     rewrite tctx_interp_cons. iIntros "[Hp HT]".
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "[% Hown]".
+    wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "% Hown".
     iDestruct "Hown" as (b) "Hv". iDestruct "Hv" as %[=->].
     destruct b; wp_if.
     - iApply (He1 with "LFT HE HL HC HT").
     - iApply (He2 with "LFT HE HL HC HT").
   Qed.
-End bool.
+End typing.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
new file mode 100644
index 0000000000000000000000000000000000000000..02ef4c9f1c06fffd3ab834c142d10ac2a586839f
--- /dev/null
+++ b/theories/typing/borrow.v
@@ -0,0 +1,143 @@
+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import big_op.
+From lrust.lifetime Require Import reborrow frac_borrow.
+From lrust.lang Require Import heap.
+From lrust.typing Require Export uniq_bor shr_bor own.
+From lrust.typing Require Import lft_contexts type_context perm typing.
+
+(** The rules for borrowing and derferencing borrowed non-Copy pointers are in
+  a separate file so make sure that own.v and uniq_bor.v can be compiled
+  concurrently. *)
+
+Section borrow.
+  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)].
+  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 "$".
+  Qed.
+  
+  Lemma tctx_reborrow_uniq E L p ty κ κ' :
+    lctx_lft_incl E L κ' κ →
+    tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)]
+                  [TCtx_hasty p (&uniq{κ'}ty); TCtx_blocked p κ (&uniq{κ}ty)].
+  Proof.
+    iIntros (Hκκ' tid ??) "#LFT HE HL H".
+    iDestruct (elctx_interp_persist with "HE") as "#HE'".
+    iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
+    iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
+    rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
+    iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l P) "[[EQ #Hiff] Hb]".
+    iDestruct "EQ" as %[=->]. iMod (bor_iff with "LFT [] Hb") as "Hb". done. by eauto.
+    iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro. iSplitL "Hb".
+    - iExists _. iSplit. done. iExists _, _. erewrite <-uPred.iff_refl. eauto.
+    - iExists _. iSplit. done. iIntros "#H†".
+      iMod ("Hext" with ">[]") as "Hb". by iApply (lft_incl_dead with "Hκκ' H†").
+      iExists _, _. erewrite <-uPred.iff_refl. eauto.
+  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 borrow.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 93aab3a0a3c30e887aff5d2ea47cd91216efc0ca..be7f6344b8f2cc3ea9becab0a665a3b923871386 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -4,7 +4,7 @@ From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
 
-Section cont_typing.
+Section typing.
   Context `{typeG Σ}.
 
   (** Jumping to and defining a continuation. *)
@@ -38,4 +38,4 @@ Section cont_typing.
     by iApply "IH".
   Qed.
 
-End cont_typing.
+End typing.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 0c6c3e17f60eb1b940027732657b48a848527b6f..44f8af549f39ed264c4b5513c9e17be6364b78f8 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -20,11 +20,15 @@ Section fn.
 
   Global Instance fn_send {A n} E tys ty : Send (@fn A n E tys ty).
   Proof. iIntros (tid1 tid2 vl). done. Qed.
+End fn.
+
+Section typing.
+  Context `{typeG Σ}.
 
-  Lemma fn_subtype_ty A n E0 L0 E tys1 tys2 ty1 ty2 :
-    (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys2 x : vec _ _) (tys1 x : vec _ _)) →
+  Lemma fn_subtype_ty {A n} E0 L0 E (tys1 : A → vec type n) tys2 ty1 ty2 :
+    (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys2 x : vec _ n) (tys1 x)) →
     (∀ x, subtype (E0 ++ E x) L0 (ty1 x) (ty2 x)) →
-    subtype E0 L0 (@fn A n E tys1 ty1) (@fn A n E tys2 ty2).
+    subtype E0 L0 (fn E tys1 ty1) (fn E tys2 ty2).
   Proof.
     intros Htys Hty. apply subtype_simple_type=>//= _ vl.
     iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
@@ -65,9 +69,9 @@ Section fn.
     iExists f. iSplit. done. rewrite /typed_body. iIntros "!# *". iApply "Hf".
   Qed.
 
-  Lemma fn_subtype_elctx_sat {A n} E0 L0 E E' tys ty :
+  Lemma fn_subtype_elctx_sat {A n} E0 L0 E E' (tys : A → vec type n) ty :
     (∀ x, elctx_sat (E x) [] (E' x)) →
-    subtype E0 L0 (@fn A n E' tys ty) (fn E tys ty).
+    subtype E0 L0 (fn E' tys ty) (fn E tys ty).
   Proof.
     intros HEE'. apply subtype_simple_type=>//= _ vl.
     iIntros "#LFT _ _ Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
@@ -78,9 +82,9 @@ Section fn.
     by iMod ("Hclose" with "HE") as "[$ _]".
   Qed.
 
-  Lemma fn_subtype_lft_incl {A n} E0 L0 E κ κ' tys ty :
+  Lemma fn_subtype_lft_incl {A n} E0 L0 E κ κ' (tys : A → vec type n) ty :
     lctx_lft_incl E0 L0 κ κ' →
-    subtype E0 L0 (@fn A n (λ x, ELCtx_Incl κ κ' :: E x) tys ty) (fn E tys ty).
+    subtype E0 L0 (fn (λ x, ELCtx_Incl κ κ' :: E x) tys ty) (fn E tys ty).
   Proof.
     intros Hκκ'. apply subtype_simple_type=>//= _ vl.
     iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
@@ -98,7 +102,7 @@ Section fn.
   Proof.
     iIntros (HTsat HEsat tid qE) "#LFT HE HL HC".
     rewrite tctx_interp_cons. iIntros "[Hf HT]".
-    wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "[% Hf]".
+    wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "% Hf".
     iMod (HTsat with "LFT HE HL HT") as "(HE & HL & HT)". rewrite tctx_interp_app.
     iDestruct "HT" as "[Hargs HT']". clear HTsat. rewrite -vec_to_list_cons.
     iApply (wp_app_vec (λ i v, match i with O => ⌜v = k⌝ ∗ _ | S i =>
@@ -113,7 +117,7 @@ Section fn.
       edestruct (lookup_lt_is_Some_2 (tys x)) as [ty Hty].
       { move: Hlen. rewrite !vec_to_list_length. done. }
       iSpecialize ("HT" with "* []"); first done.
-      iApply (wp_hasty with "HT"). iIntros (v') "[% Hown]". iIntros (ty') "#EQ".
+      iApply (wp_hasty with "HT"). iIntros (v') "% Hown". iIntros (ty') "#EQ".
       rewrite Hty. iDestruct "EQ" as %[=<-]. iExists v'. iFrame "Hown".
       iPureIntro. exact: eval_path_of_val.
     - iIntros (vl'). assert (Hvl := Vector.eta vl'). remember (Vector.hd vl') as kv.
@@ -156,4 +160,4 @@ Section fn.
     rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
     iApply tctx_send. by iNext.
   Qed.
-End fn.
+End typing.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index b4d751e782b204ef01ed9bf8a625bf576180d7bd..da436078dd384c29c911d5f0d03eee627c9c074d 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -11,6 +11,10 @@ Section int.
 
   Global Instance int_send : Send int.
   Proof. iIntros (tid1 tid2 vl). done. Qed.
+End int.
+
+Section typing.
+  Context `{typeG Σ}.
 
   Lemma type_int (z : Z) E L :
     typed_instruction_ty E L [] #z int.
@@ -24,8 +28,8 @@ Section int.
   Proof.
     iIntros (tid qE) "!# _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
-    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "[% Hown1]".
-    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "[% Hown2]".
+    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
+    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "% Hown2".
     iDestruct "Hown1" as (z1) "EQ". iDestruct "EQ" as %[=->].
     iDestruct "Hown2" as (z2) "EQ". iDestruct "EQ" as %[=->].
     wp_op. rewrite tctx_interp_singleton. iExists _. iSplitR; first done.
@@ -37,8 +41,8 @@ Section int.
   Proof.
     iIntros (tid qE) "!# _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
-    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "[% Hown1]".
-    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "[% Hown2]".
+    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
+    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "% Hown2".
     iDestruct "Hown1" as (z1) "EQ". iDestruct "EQ" as %[=->].
     iDestruct "Hown2" as (z2) "EQ". iDestruct "EQ" as %[=->].
     wp_op. rewrite tctx_interp_singleton. iExists _. iSplitR; first done.
@@ -50,12 +54,12 @@ Section int.
   Proof.
     iIntros (tid qE) "!# _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
-    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "[% Hown1]".
-    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "[% Hown2]".
+    wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
+    wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "% Hown2".
     iDestruct "Hown1" as (z1) "EQ". iDestruct "EQ" as %[=->].
     iDestruct "Hown2" as (z2) "EQ". iDestruct "EQ" as %[=->].
     wp_op; intros _; rewrite tctx_interp_singleton; iExists _; (iSplitR; first done);
       iExists _; done.
   Qed.
   
-End int.
+End typing.
diff --git a/theories/typing/mem.v b/theories/typing/mem.v
deleted file mode 100644
index 46b9d79d0d6241cf6aecdecb5ef14bfe81f1ab1f..0000000000000000000000000000000000000000
--- a/theories/typing/mem.v
+++ /dev/null
@@ -1,239 +0,0 @@
-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 update_strong ty1 ty2 n:
-    ty1.(ty_size) = ty2.(ty_size) →
-    update ty1 (λ ν, ν ◁ own n ty2)%P (λ ν, ν ◁ own n ty1)%P.
-  Proof.
-    iIntros (Hsz ν tid Φ E ?) "_ H◁ 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↦ & >H†)".
-    iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    rewrite ty2.(ty_size_eq) -Hsz. iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%".
-    iIntros (vl') "[H↦ Hown']!>". rewrite /has_type Hνv.
-    iExists _. iSplit. done. iFrame. iExists _. iFrame.
-  Qed.
-
-  Lemma consumes_copy_own ty n:
-    Copy ty → consumes ty (λ ν, ν ◁ own n ty)%P (λ ν, ν ◁ own n ty)%P.
-  Proof.
-    iIntros (? ν tid Φ E ?) "_ H◁ 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↦ & >H†)".
-    iDestruct "Heq" as %[=->]. 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↦!>".
-    rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
-  Qed.
-
-  Lemma consumes_move ty n:
-    consumes ty (λ ν, ν ◁ own n ty)%P (λ ν, ν ◁ own n (uninit ty.(ty_size)))%P.
-  Proof.
-    iIntros (ν tid Φ E ?) "_ H◁ 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↦ & >H†)".
-    iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">Hlen".
-      by rewrite ty.(ty_size_eq). iDestruct "Hlen" as %Hlen.
-    iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
-    rewrite /has_type Hνv. iExists _. iSplit. done. iSplitR "H†".
-    - rewrite -Hlen. iExists vl. iIntros "{$H↦}!>". clear.
-      iInduction vl as [|v vl] "IH". done.
-      iExists [v], vl. iSplit. done. by iSplit.
-    - rewrite uninit_sz; auto.
-  Qed.
-
-
-  Lemma consumes_copy_uniq_bor `(!Copy ty) κ κ' q:
-    consumes ty (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
-                (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
-  Proof.
-    iIntros (ν tid Φ E ?) "#LFT (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' 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]". set_solver.
-    iMod (bor_acc with "LFT 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 ("Hclose'" with "[H↦]") as "[H↦ Htok]". by iExists _; iFrame.
-    iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv.
-    iExists _, _. erewrite <-uPred.iff_refl. auto.
-  Qed.
-
-  Lemma update_weak ty q κ κ':
-    update ty (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
-              (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
-  Proof.
-    iIntros (ν tid Φ E ?) "#LFT (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 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]". set_solver.
-    iMod (bor_acc with "LFT 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 ("Hclose'" with "[H↦ Hown]") as "[Hbor Htok]". by iExists _; iFrame.
-    iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv.
-    iExists _, _. erewrite <-uPred.iff_refl. auto.
-  Qed.
-
-  Lemma consumes_copy_shr_bor ty κ κ' q:
-    Copy ty →
-    consumes ty (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
-                (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
-  Proof.
-    iIntros (? ν tid Φ E ?) "#LFT (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_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
-    iMod (copy_shr_acc with "LFT Hshr Htok Htl") as (q'') "(H↦ & Htl & Hclose')".
-    { assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
-    { done. }
-    iDestruct "H↦" as (vl) "[>H↦ #Hown]".
-    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
-      by rewrite ty.(ty_size_eq).
-    iModIntro. iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
-    iMod ("Hclose'" with "[H↦] Htl") as "[Htok $]". iExists _; by iFrame.
-    iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
-  Qed.
-
-  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 9d99636c122de4f78a68b0ce0c1b2cdaace2336a..3ed5b861485efe8b61991555e0b5f53513835c73 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -4,7 +4,7 @@ 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.typing Require Export type.
-From lrust.typing Require Import uniq_bor type_context.
+From lrust.typing Require Import uninit type_context programs perm typing.
 
 Section own.
   Context `{typeG Σ}.
@@ -133,21 +133,88 @@ Section own.
     iClear "Hshr". (* FIXME: Using "{HShr} [HShr $]" for the intro pattern in the following line doesn't work. *)
     iMod "Hfin" as "[Hshr $]". by iApply Hsync.
   Qed.
+End own.
+
+Section typing.
+  Context `{typeG Σ}.
 
   (** 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)].
+  Lemma write_own E L ty ty' n :
+    ty.(ty_size) = ty'.(ty_size) → typed_writing E L (own n ty') ty (own n 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 (Hsz p tid Φ F ?) "_ Hp HΦ". iApply wp_fupd. iApply (wp_hasty with "Hp").
+    iIntros (v) "Hp Hown". iDestruct "Hp" as %Hp.
+    iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
+    iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
+    rewrite ty'.(ty_size_eq). (* This turns out to be the fastest way to apply a lemma below â–· -- at least if we're fine throwing away the premise even though the result is persistent, which in this case, we are. *)
+    iDestruct "Hown" as ">%".
+    iApply ("HΦ" with "* [%] [] H↦"); [congruence|done|].
+    iIntros (vl') "H↦ Hown' !>". iExists _. iSplit; first done.
+    iExists _. iSplit; first done. rewrite Hsz. iFrame "H†".
+    iExists _. iFrame.
   Qed.
 
+  (* Old Typing *)
 
-End own.
+  Lemma consumes_copy_own ty n:
+    Copy ty → consumes ty (λ ν, ν ◁ own n ty)%P (λ ν, ν ◁ own n ty)%P.
+  Proof.
+    iIntros (? ν tid Φ E ?) "_ H◁ 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↦ & >H†)".
+    iDestruct "Heq" as %[=->]. 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↦!>".
+    rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
+  Qed.
+
+
+  Lemma consumes_move ty n:
+    consumes ty (λ ν, ν ◁ own n ty)%P (λ ν, ν ◁ own n (uninit ty.(ty_size)))%P.
+  Proof.
+    iIntros (ν tid Φ E ?) "_ H◁ 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↦ & >H†)".
+    iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
+    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">Hlen".
+      by rewrite ty.(ty_size_eq). iDestruct "Hlen" as %Hlen.
+    iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
+    rewrite /has_type Hνv. iExists _. iSplit. done. iSplitR "H†".
+    - rewrite -Hlen. iExists vl. iIntros "{$H↦}!>". clear.
+      iInduction vl as [|v vl] "IH". done.
+      iExists [v], vl. iSplit. done. by iSplit.
+    - rewrite uninit_sz; auto.
+  Qed.
+
+
+  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.
+
+
+End typing.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 59be09e5253f489eadf02c75847e18485a279f0f..9ae5f73f11147bd6b4d119f980810ccba2e25cda 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -43,6 +43,16 @@ Section typing.
     (∀ tid qE, □ (lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗ tctx_interp tid T1 -∗
                    WP e {{ v, elctx_interp E qE ∗ llctx_interp L 1 ∗ tctx_interp tid (T2 v) }}))%I.
   Global Arguments typed_instruction _ _ _ _%E _.
+
+  (** Writing and Reading **)
+  Definition typed_writing (E : elctx) (L : llctx) (ty1 ty ty2 : type) : Prop :=
+    ∀ p tid Φ E, lftE ∪ (↑lrustN) ⊆ E →
+      lft_ctx -∗ tctx_elt_interp tid (TCtx_hasty p ty1) -∗
+      (∀ (l:loc) vl,
+         ⌜length vl = ty.(ty_size)⌝ -∗ ⌜eval_path p = Some #l⌝ -∗ l ↦∗ vl -∗
+           (∀ vl', l ↦∗ vl' -∗ ▷ (ty.(ty_own) tid vl') ={E}=∗
+                           tctx_elt_interp tid (TCtx_hasty p ty2)) -∗ Φ #l) -∗
+      WP p @ E {{ Φ }}.
 End typing.
 
 Notation typed_instruction_ty E L T1 e ty := (typed_instruction E L T1 e (λ v : val, [TCtx_hasty v ty])).
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 2f8af2758859db5a76c41943ccc69a46c8efd491..0fea6057811bb9440056688a672aa7d6590715db 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -63,4 +63,27 @@ Section typing.
       iExists _. auto.
   Qed.
 
+  (* Old typing *)
+  
+  Lemma consumes_copy_shr_bor ty κ κ' q:
+    Copy ty →
+    consumes ty (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
+                (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
+  Proof.
+    iIntros (? ν tid Φ E ?) "#LFT (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_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
+    iMod (copy_shr_acc with "LFT Hshr Htok Htl") as (q'') "(H↦ & Htl & Hclose')".
+    { assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. set_solver. } (* FIXME: some tactic should solve this in one go. *)
+    { done. }
+    iDestruct "H↦" as (vl) "[>H↦ #Hown]".
+    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
+      by rewrite ty.(ty_size_eq).
+    iModIntro. iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
+    iMod ("Hclose'" with "[H↦] Htl") as "[Htok $]". iExists _; by iFrame.
+    iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
+  Qed.
+
+
 End typing.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 67e025dda6ee4e71291e4bc65fb56106ab0113bc..f4fbc0a1ba06e86f0daf0de75f5e2f01485fa171 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -107,8 +107,8 @@ Section type_context.
     tctx_elt_interp tid (TCtx_hasty p2 ty).
   Proof. intros Hp. rewrite /tctx_elt_interp /=. setoid_rewrite Hp. done. Qed.
 
-  Lemma wp_eval_path p v :
-    eval_path p = Some v → (WP p {{ v', ⌜v' = v⌝ }})%I.
+  Lemma wp_eval_path E p v :
+    eval_path p = Some v → (WP p @ E {{ v', ⌜v' = v⌝ }})%I.
   Proof.
     revert v; induction p; intros v; cbn -[to_val];
       try (intros ?; by iApply wp_value); [].
@@ -124,15 +124,14 @@ Section type_context.
     iIntros (v) "%". subst v. wp_op. done.
   Qed.
 
-  Lemma wp_hasty tid p ty Φ :
+  Lemma wp_hasty E tid p ty Φ :
     tctx_elt_interp tid (TCtx_hasty p ty) -∗
-    (∀ v, ⌜eval_path p = Some v⌝ ∗ ty.(ty_own) tid [v] -∗ Φ v) -∗
-    WP p {{ Φ }}.
+    (∀ v, ⌜eval_path p = Some v⌝ -∗ ty.(ty_own) tid [v] -∗ Φ v) -∗
+    WP p @ E {{ Φ }}.
   Proof.
     iIntros "Hty HΦ". iDestruct "Hty" as (v) "[% Hown]".
-    iApply (wp_wand with "[]").
-    { iApply wp_eval_path. done. }
-    iIntros (v') "%". subst v'. iApply "HΦ". by auto.
+    iApply (wp_wand with "[]"). { iApply wp_eval_path. done. }
+    iIntros (v') "%". subst v'. iApply ("HΦ" with "* [] Hown"). by auto.
   Qed.
 
   Lemma contains_tctx_incl E L T1 T2 : T1 `contains` T2 → tctx_incl E L T2 T1.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 510c204e0aa9b7225665b7268c6cd4301b6986d3..49a0718cb9e982f81a13661af25594177d25fede 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -1,9 +1,9 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lifetime Require Import borrow reborrow frac_borrow.
+From lrust.lifetime Require Import borrow frac_borrow reborrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
-From lrust.typing Require Import lft_contexts type_context shr_bor.
+From lrust.typing Require Import lft_contexts type_context shr_bor perm typing.
 
 Section uniq_bor.
   Context `{typeG Σ}.
@@ -146,23 +146,47 @@ Section typing.
     iIntros "!>/=". eauto.
   Qed.
 
-  Lemma tctx_reborrow_uniq E L p ty κ κ' :
-    lctx_lft_incl E L κ' κ →
-    tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)]
-                  [TCtx_hasty p (&uniq{κ'}ty); TCtx_blocked p κ (&uniq{κ}ty)].
+  (* Old typing *)
+  
+
+  Lemma consumes_copy_uniq_bor `(!Copy ty) κ κ' q:
+    consumes ty (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
+                (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
+  Proof.
+    iIntros (ν tid Φ E ?) "#LFT (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' 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]". set_solver.
+    iMod (bor_acc with "LFT 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 ("Hclose'" with "[H↦]") as "[H↦ Htok]". by iExists _; iFrame.
+    iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv.
+    iExists _, _. erewrite <-uPred.iff_refl. auto.
+  Qed.
+
+
+  Lemma update_weak ty q κ κ':
+    update ty (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
+              (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
-    iIntros (Hκκ' tid ??) "#LFT HE HL H".
-    iDestruct (elctx_interp_persist with "HE") as "#HE'".
-    iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
-    iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
-    rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
-    iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l P) "[[EQ #Hiff] Hb]".
-    iDestruct "EQ" as %[=->]. iMod (bor_iff with "LFT [] Hb") as "Hb". done. by eauto.
-    iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro. iSplitL "Hb".
-    - iExists _. iSplit. done. iExists _, _. erewrite <-uPred.iff_refl. eauto.
-    - iExists _. iSplit. done. iIntros "#H†".
-      iMod ("Hext" with ">[]") as "Hb". by iApply (lft_incl_dead with "Hκκ' H†").
-      iExists _, _. erewrite <-uPred.iff_refl. eauto.
+    iIntros (ν tid Φ E ?) "#LFT (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 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]". set_solver.
+    iMod (bor_acc with "LFT 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 ("Hclose'" with "[H↦ Hown]") as "[Hbor Htok]". by iExists _; iFrame.
+    iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv.
+    iExists _, _. erewrite <-uPred.iff_refl. auto.
   Qed.
 
+
 End typing.