diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index d84c70a2a801fd6108674498eb37bf145f0abbca..65de7b92faae3a77fc36ab5e13bf422cb9597ae5 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -19,7 +19,7 @@ Section typing.
   Lemma type_bool (b : Datatypes.bool) E L :
     typed_instruction_ty E L [] #b bool.
   Proof.
-    iIntros (tid qE) "_ _ $ $ _". wp_value.
+    iIntros (tid qE) "_ _ $ $ $ _". wp_value.
     rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
   Qed.
 
@@ -28,12 +28,12 @@ Section typing.
     typed_body E L C (TCtx_hasty p bool :: T) (if: p then e1 else e2).
   Proof.
     (* FIXME why can't I merge these two iIntros? *)
-    iIntros (He1 He2). iIntros (tid qE) "#HEAP #LFT HE HL HC".
+    iIntros (He1 He2). iIntros (tid qE) "#HEAP #LFT Htl HE HL HC".
     rewrite tctx_interp_cons. iIntros "[Hp HT]".
     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 "HEAP LFT HE HL HC HT").
-    - iApply (He2 with "HEAP LFT HE HL HC HT").
+    - iApply (He1 with "HEAP LFT Htl HE HL HC HT").
+    - iApply (He2 with "HEAP LFT Htl HE HL HC HT").
   Qed.
 End typing.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 4189b54328cd960d1c460e3f820457332efcbf36..7128abf69c242f72b820e3eb7e0b5cec0dbef886 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -12,10 +12,10 @@ Section typing.
     tctx_incl E L T (T' args) →
     typed_body E L [CCtx_iscont k L n T'] T (k (of_val <$> (args : list _))).
   Proof.
-    iIntros (Hincl tid qE) "#HEAP #LFT HE HL HC HT".
+    iIntros (Hincl tid qE) "#HEAP #LFT Htl HE HL HC HT".
     iMod (Hincl with "LFT HE HL HT") as "(HE & HL & HT)".
     iSpecialize ("HC" with "HE * []"); first by (iPureIntro; apply elem_of_list_singleton).
-    simpl. iApply ("HC" with "* HL HT").
+    simpl. iApply ("HC" with "* Htl HL HT").
   Qed.
 
   Lemma type_cont {n} E L1 L2 C T T' kb (argsb : vec binder n) e1 econt e2 :
@@ -25,16 +25,16 @@ Section typing.
     (∀ k, typed_body E (L1 ++ L2) (CCtx_iscont k L1 n T' :: C) T (subst' kb k e2)) →
     typed_body E (L1 ++ L2) C T (let: kb := e1 in e2).
   Proof.
-    iIntros (-> Hc1 Hc2 Hecont He2 tid qE) "#HEAP #LFT HE HL HC HT". iApply wp_let'.
+    iIntros (-> Hc1 Hc2 Hecont He2 tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
     { simpl. rewrite decide_left. done. }
-    iModIntro. iApply (He2 with "* HEAP LFT HE HL [HC] HT"). clear He2.
+    iModIntro. iApply (He2 with "* HEAP LFT Htl HE HL [HC] HT"). clear He2.
     iIntros "HE". iLöb as "IH". iIntros (x) "H".
     iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE *").
-    iIntros (args) "HL HT". iApply wp_rec; try done.
+    iIntros (args) "Htl HL HT". iApply wp_rec; try done.
     { apply Forall_of_val_is_val. }
     { rewrite -vec_to_list_map -subst_vec_eq. eauto. }
     (* FIXME: iNext here unfolds things in the context. *)
-    iNext. iApply (Hecont with "* HEAP LFT HE HL [HC] HT").
+    iNext. iApply (Hecont with "* HEAP LFT Htl HE HL [HC] HT").
     by iApply "IH".
   Qed.
 
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 1a58e6900dd5a431dae17aa2df2ebf5274bb0c7b..9bd73963486768785bf088d3c356f562d6a43fda 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -21,7 +21,7 @@ Section cont_context.
 
   Definition cctx_elt_interp (tid : thread_id) (x : cctx_elt) : iProp Σ :=
     let 'CCtx_iscont k L n T := x in
-    (∀ args, llctx_interp L 1 -∗ tctx_interp tid (T args) -∗
+    (∀ args, na_own tid ⊤ -∗ llctx_interp L 1 -∗ tctx_interp tid (T args) -∗
          WP k (of_val <$> (args : list _)) {{ _, cont_postcondition }})%I.
   Definition cctx_interp (tid : thread_id) (C : cctx) : iProp Σ :=
     (∀ (x : cctx_elt), ⌜x ∈ C⌝ -∗ cctx_elt_interp tid x)%I.
@@ -62,10 +62,10 @@ Section cont_context.
   Proof.
     iIntros (HC1C2 HT1T2 ??) "#LFT H HE". rewrite /cctx_interp.
     iIntros (x) "Hin". iDestruct "Hin" as %[->|Hin]%elem_of_cons.
-    - iIntros (args) "HL HT".
+    - iIntros (args) "Htl HL HT".
       iMod (HT1T2 with "LFT HE HL HT") as "(HE & HL & HT)".
       iSpecialize ("H" with "HE").
-      iApply ("H" $! (CCtx_iscont _ _ _ _) with "[%] * HL HT").
+      iApply ("H" $! (CCtx_iscont _ _ _ _) with "[%] * Htl HL HT").
       constructor.
     - iApply (HC1C2 with "LFT [H] HE * [%]"); last done.
       iIntros "HE". iIntros (x') "%".
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 7255a4e597cc86993c1a99b473b0a833939340b5..dfea82ae1172ecae5c040f78112ae2b4162fc4a1 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -32,14 +32,14 @@ Section typing.
   Proof.
     intros Htys Hty. apply subtype_simple_type=>//= _ vl.
     iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
-    iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ HE HL HC HT".
+    iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ Htl HE HL HC HT".
     iDestruct (elctx_interp_persist with "HE") as "#HE'".
-    iApply ("Hf" with "* HEAP LFT HE HL [HC] [HT]").
+    iApply ("Hf" with "* HEAP LFT Htl HE HL [HC] [HT]").
     - iIntros "HE". unfold cctx_interp. iIntros (e) "He".
-      iDestruct "He" as %->%elem_of_list_singleton. iIntros (ret) "HL HT".
+      iDestruct "He" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
       iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
-      iApply ("HC" $! (CCtx_iscont _ _ _ _) with "[%] * HL >").
-        by apply elem_of_list_singleton.
+      iApply ("HC" $! (CCtx_iscont _ _ _ _) with "[%] * Htl HL >").
+      {  by apply elem_of_list_singleton. }
       rewrite /tctx_interp !big_sepL_singleton /=.
       iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
       iDestruct (Hty x with "LFT [HE0 HE'] HL0") as "(_ & #Hty & _)".
@@ -75,9 +75,9 @@ Section typing.
   Proof.
     intros HEE'. apply subtype_simple_type=>//= _ vl.
     iIntros "#LFT _ _ Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
-    iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ HE #HL HC HT".
+    iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ Htl HE #HL HC HT".
     iMod (HEE' x with "[%] HE HL") as (qE') "[HE Hclose]". done.
-    iApply ("Hf" with "* HEAP LFT HE HL [Hclose HC] HT"). iIntros "HE".
+    iApply ("Hf" with "* HEAP LFT Htl HE HL [Hclose HC] HT"). iIntros "HE".
     iApply fupd_cctx_interp. iApply ("HC" with ">").
     by iMod ("Hclose" with "HE") as "[$ _]".
   Qed.
@@ -88,8 +88,8 @@ Section typing.
   Proof.
     intros Hκκ'. apply subtype_simple_type=>//= _ vl.
     iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (f) "[% #Hf]". subst.
-    iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ HE #HL HC HT".
-    iApply ("Hf" with "* HEAP LFT [HE] HL [HC] HT").
+    iExists f. iSplit. done. rewrite /typed_body. iIntros "!# * #HEAP _ Htl HE #HL HC HT".
+    iApply ("Hf" with "* HEAP LFT Htl [HE] HL [HC] HT").
     { rewrite /elctx_interp big_sepL_cons. iFrame. iApply (Hκκ' with "HE0 HL0"). }
     rewrite /elctx_interp big_sepL_cons. iIntros "[_ HE]". by iApply "HC".
   Qed.
@@ -100,7 +100,7 @@ Section typing.
     typed_body E L [CCtx_iscont k L 1 (λ v, (TCtx_hasty (v!!!0) (ty x)) :: T')]
                (TCtx_hasty p (fn E' tys ty) :: T) (p (of_val k :: ps)).
   Proof.
-    iIntros (HTsat HEsat tid qE) "#HEAP #LFT HE HL HC".
+    iIntros (HTsat HEsat tid qE) "#HEAP #LFT Htl HE HL HC".
     rewrite tctx_interp_cons. iIntros "[Hf HT]".
     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.
@@ -126,13 +126,13 @@ Section typing.
       iDestruct "Hf" as (f) "[EQ #Hf]". iDestruct "EQ" as %[=->].
       iSpecialize ("Hf" $! x vl k). 
       iMod (HEsat with "[%] HE HL") as (q') "[HE' Hclose]"; first done.
-      iApply ("Hf" with "HEAP LFT HE' [] [HC Hclose HT']").
+      iApply ("Hf" with "HEAP LFT Htl HE' [] [HC Hclose HT']").
       + by rewrite /llctx_interp big_sepL_nil.
       + iIntros "HE'". iApply fupd_cctx_interp. iMod ("Hclose" with "HE'") as "[HE HL]".
         iSpecialize ("HC" with "HE").  iModIntro. iIntros (y) "IN".
         iDestruct "IN" as %->%elem_of_list_singleton.
-        iIntros (args) "_ HT". iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton).
-        iApply ("HC" $! args with "HL"). rewrite tctx_interp_singleton tctx_interp_cons.
+        iIntros (args) "Htl _ HT". iSpecialize ("HC" with "* []"); first by (iPureIntro; apply elem_of_list_singleton).
+        iApply ("HC" $! args with "Htl HL"). rewrite tctx_interp_singleton tctx_interp_cons.
         iFrame.
       + rewrite /tctx_interp big_sepL_zip_with. done.
   Qed.
@@ -147,16 +147,16 @@ Section typing.
                  (subst' fb f $ subst_vec (kb ::: argsb) (Vector.map of_val $ k ::: args) e)) →
     typed_instruction_ty E L (zip_with TCtx_hasty cps ctyl) ef (fn E' tys ty).
   Proof.
-    iIntros (-> Hc Hbody tid qE) "#HEAP #LFT $ $ #HT". iApply wp_value.
+    iIntros (-> Hc Hbody tid qE) "#HEAP #LFT $ $ $ #HT". iApply wp_value.
     { simpl. rewrite decide_left. done. }
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
     { simpl. rewrite decide_left. done. }
     iExists _. iSplit; first done. iAlways. clear qE. 
-    iIntros (x args k). iIntros (tid' qE) "_ _ HE HL HC HT'".
+    iIntros (x args k). iIntros (tid' qE) "_ _ Htl HE HL HC HT'".
     iApply wp_rec; try done.
     { apply Forall_of_val_is_val. }
     { rewrite -!vec_to_list_cons -vec_to_list_map -subst_vec_eq. eauto. }
-    iApply (Hbody with "* HEAP LFT HE HL HC").
+    iApply (Hbody with "* HEAP LFT Htl HE HL HC").
     rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
     iApply tctx_send. by iNext.
   Qed.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index fa0559634a6a924e1fd6751ac4094591a4903630..407ec159786f842ce0abde2e63ac312f41acf911 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -19,14 +19,14 @@ Section typing.
   Lemma type_int (z : Z) E L :
     typed_instruction_ty E L [] #z int.
   Proof.
-    iIntros (tid qE) "_ _ $ $ _". wp_value.
+    iIntros (tid qE) "_ _ $ $ $ _". wp_value.
     rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
   Qed.
 
   Lemma type_plus E L p1 p2 :
     typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 + p2) int.
   Proof.
-    iIntros (tid qE) "_ _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+    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".
@@ -39,7 +39,7 @@ Section typing.
   Lemma type_minus E L p1 p2 :
     typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 - p2) int.
   Proof.
-    iIntros (tid qE) "_ _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+    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".
@@ -52,7 +52,7 @@ Section typing.
   Lemma type_le E L p1 p2 :
     typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 ≤ p2) bool.
   Proof.
-    iIntros (tid qE) "_ _ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+    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".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 9bf736d05d4e1c45c6cd5a815c33623a65f608ac..7a7876382a8e8fd8fce9dbc9336b92aa79a54e1b 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -153,7 +153,7 @@ Section typing.
   Lemma read_own_copy E L ty n :
     Copy ty → typed_read E L (own n ty) ty (own n ty).
   Proof.
-    iIntros (Hsz p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
+    iIntros (Hsz p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]". iModIntro.
     iExists l, _, _. iSplit; first done. iFrame "∗#". iIntros "Hl !>".
     iExists _. iSplit; first done. iFrame "H†". iExists _. by iFrame.
@@ -162,7 +162,7 @@ Section typing.
   Lemma read_own_move E L ty n :
     typed_read E L (own n ty) ty (own n $ uninit ty.(ty_size)).
   Proof.
-    iIntros (p tid F qE qL ?) "_ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
+    iIntros (p tid F qE qL ?) "_ $ $ $ Hown". iDestruct "Hown" as (l) "(Heq & H↦ & H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
     { by iApply ty_size_eq. }
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 36c39d94dcca39718309f22bcf55f94f8264c57f..e1d8f2ce3ed62d24afb3cfa28ef7d2ed59443bda 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -13,11 +13,11 @@ Section product.
 
   Global Instance unit_copy : Copy unit.
   Proof.
-    split. by apply _. iIntros (????????) "_ _ $ Htok".
+    split. by apply _. iIntros (????????) "_ _ Htok $".
     iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first set_solver+.
     iExists 1%Qp. iModIntro. iSplitR.
     { iExists []. iSplitL; last by auto. rewrite heap_mapsto_vec_nil. auto. }
-    iIntros "_ Htok2". iApply "Htok". done.
+    iIntros "Htok2 _". iApply "Htok". done.
   Qed.
 
   Global Instance unit_send : Send unit.
@@ -89,10 +89,10 @@ Section product.
     Copy (product2 ty1 ty2).
   Proof.
     split; first (intros; apply _).
-    intros κ tid E F l q ? HF. iIntros "#LFT [H1 H2] [Htok1 Htok2] Htl".
-    iMod (@copy_shr_acc with "LFT H1 Htok1 Htl") as (q1) "(H1 & Htl & Hclose1)"; first set_solver.
+    intros κ tid E F l q ? HF. iIntros "#LFT [H1 H2] Htl [Htok1 Htok2]".
+    iMod (@copy_shr_acc with "LFT H1 Htl Htok1") as (q1) "(Htl & H1 & Hclose1)"; first set_solver.
     { rewrite <-HF. apply shr_locsE_subseteq. simpl. clear. omega. }
-    iMod (@copy_shr_acc with "LFT H2 Htok2 Htl") as (q2) "(H2 & Htl & Hclose2)"; first set_solver.
+    iMod (@copy_shr_acc with "LFT H2 Htl Htok2") as (q2) "(Htl & H2 & Hclose2)"; first set_solver.
     { move: HF. rewrite /= -plus_assoc shr_locsE_shift.
       assert (shr_locsE l (ty_size ty1) ⊥ shr_locsE (shift_loc l (ty_size ty1)) (ty_size ty2 + 1))
              by exact: shr_locsE_disj.
@@ -109,7 +109,7 @@ Section product.
     iDestruct "H↦1" as "[H↦1 H↦1f]". iDestruct "H↦2" as "[H↦2 H↦2f]".
     iIntros "!>". iSplitL "H↦1 H1 H↦2 H2".
     - iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame.
-    - iIntros "[H1 H2] Htl". iDestruct ("Htlclose" with "Htl") as "Htl".
+    - iIntros "Htl [H1 H2]". iDestruct ("Htlclose" with "Htl") as "Htl".
       iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
       iAssert (▷ ⌜length vl1' = ty1.(ty_size)⌝)%I with "[#]" as ">%".
       { iNext. by iApply ty_size_eq. }
@@ -118,8 +118,8 @@ Section product.
       iCombine "H↦1" "H↦1f" as "H↦1". iCombine "H↦2" "H↦2f" as "H↦2".
       rewrite !heap_mapsto_vec_op; try by congruence.
       iDestruct "H↦1" as "[_ H↦1]". iDestruct "H↦2" as "[_ H↦2]".
-      iMod ("Hclose2" with "[H2 H↦2] Htl") as "[$ Htl]". by iExists _; iFrame.
-      iMod ("Hclose1" with "[H1 H↦1] Htl") as "[$$]". by iExists _; iFrame. done.
+      iMod ("Hclose2" with "Htl [H2 H↦2]") as "[Htl $]". by iExists _; iFrame.
+      iMod ("Hclose1" with "Htl [H1 H↦1]") as "[$$]". by iExists _; iFrame. done.
   Qed.
 
   Global Instance product2_send `{!Send ty1} `{!Send ty2} :
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index d72cbc4b83ebfa91bd3662f8da0087c63a5b4346..25ba68e7e4b60b1b3e27349d2c530df36ebcb7ef 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -11,7 +11,7 @@ Section typing.
   (* This is an iProp because it is also used by the function type. *)
   Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
                         (e : expr) : iProp Σ :=
-    (∀ tid qE, heap_ctx -∗ lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗
+    (∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗
                (elctx_interp E qE -∗ cctx_interp tid C) -∗ tctx_interp tid T -∗
                WP e {{ _, cont_postcondition }})%I.
   Global Arguments typed_body _ _ _ _ _%E.
@@ -32,17 +32,18 @@ Section typing.
     Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢)) (typed_body E L).
   Proof.
     intros C1 C2 HC T1 T2 HT e ? <-. iIntros "H".
-    iIntros (tid qE) "#HEAP #LFT HE HL HC HT".
+    iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
     iMod (HT with "LFT HE HL HT") as "(HE & HL & HT)".
-    iApply ("H" with "HEAP LFT HE HL [HC] HT").
+    iApply ("H" with "HEAP LFT Htl HE HL [HC] HT").
     iIntros "HE". by iApply (HC with "LFT HC").
   Qed.
 
   (** Instruction *)
   Definition typed_instruction (E : elctx) (L : llctx)
              (T1 : tctx) (e : expr) (T2 : val → tctx) : Prop :=
-    ∀ tid qE, heap_ctx -∗ 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) }}.
+    ∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗
+              elctx_interp E qE -∗ llctx_interp L 1 -∗ tctx_interp tid T1 -∗ 
+                   WP e {{ v, na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L 1 ∗ tctx_interp tid (T2 v) }}.
   Global Arguments typed_instruction _ _ _ _%E _.
 
   (** Writing and Reading **)
@@ -60,9 +61,9 @@ Section typing.
      fraction was given). So we go with the definition that is easier to prove. *)
   Definition typed_read (E : elctx) (L : llctx) (ty1 ty ty2 : type) : Prop :=
     ∀ v tid F qE qL, lftE ∪ (↑lrustN) ⊆ F →
-      lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
+      lft_ctx -∗ na_own tid F -∗ elctx_interp E qE -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
         ∃ (l : loc) vl q, ⌜v = #l⌝ ∗ l ↦∗{q} vl ∗ ▷ ty.(ty_own) tid vl ∗
-          (l ↦∗{q} vl ={F}=∗ elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]).
+          (l ↦∗{q} vl ={F}=∗ na_own tid F ∗ elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]).
 End typing.
 
 Notation typed_instruction_ty E L T1 e ty := (typed_instruction E L T1 e (λ v : val, [TCtx_hasty v ty])).
@@ -76,11 +77,11 @@ Section typing_rules.
     (∀ v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) →
     typed_body E L C (T1 ++ T) (let: xb := e in e').
   Proof.
-    iIntros (Hc He He' tid qE) "#HEAP #LFT HE HL HC HT". rewrite tctx_interp_app.
-    iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[HE HL HT1]").
-    { iApply (He with "HEAP LFT HE HL HT1"). }
-    iIntros (v) "/= (HE & HL & HT2)". iApply wp_let; first wp_done. iModIntro.
-    iApply (He' with "HEAP LFT HE HL HC [HT2 HT]"). rewrite tctx_interp_app. by iFrame.
+    iIntros (Hc He He' tid qE) "#HEAP #LFT Htl HE HL HC HT". rewrite tctx_interp_app.
+    iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[HE HL HT1 Htl]").
+    { iApply (He with "HEAP LFT Htl HE HL HT1"). }
+    iIntros (v) "/= (Htl & HE & HL & HT2)". iApply wp_let; first wp_done. iModIntro.
+    iApply (He' with "HEAP LFT Htl HE HL HC [HT2 HT]"). rewrite tctx_interp_app. by iFrame.
   Qed.
   
   Lemma type_assign E L ty1 ty ty1' p1 p2 :
@@ -88,7 +89,7 @@ Section typing_rules.
     typed_instruction E L [TCtx_hasty p1 ty1; TCtx_hasty p2 ty] (p1 <- p2)
                       (λ _, [TCtx_hasty p1 ty1']).
   Proof.
-    iIntros (Hwrt tid qE) "#HEAP #LFT HE HL".
+    iIntros (Hwrt tid qE) "#HEAP #LFT $ HE HL".
     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".
@@ -108,9 +109,9 @@ Section typing_rules.
     typed_instruction E L [TCtx_hasty p ty1] (!p)
                       (λ v, [TCtx_hasty p ty1'; TCtx_hasty v ty]).
   Proof.
-    iIntros (Hsz Hread tid qE) "#HEAP #LFT HE HL Hp". rewrite tctx_interp_singleton.
+    iIntros (Hsz Hread tid qE) "#HEAP #LFT Htl HE HL Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "% Hown".
-    iMod (Hread with "* LFT HE HL Hown") as (l vl q) "(% & Hl & Hown & Hclose)"; first done.
+    iMod (Hread with "* LFT Htl HE HL Hown") as (l vl q) "(% & Hl & Hown & Hclose)"; first done.
     subst v. iAssert (▷⌜length vl = 1%nat⌝)%I with "[#]" as ">%".
     { rewrite -Hsz. iApply ty_size_eq. done. }
     destruct vl as [|v [|]]; try done.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 0fea6057811bb9440056688a672aa7d6590715db..1e63f7aa04deac2b60091ebead5a2c5b20f5c4e9 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.
+From lrust.typing Require Import lft_contexts type_context programs.
 
 Section shr_bor.
   Context `{typeG Σ}.
@@ -63,27 +63,20 @@ 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.
+  Lemma read_shr E L κ ty :
+    Copy ty → lctx_lft_alive E L κ → typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
   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.
+    iIntros (Hcopy Halive v tid F qE qL ?) "#LFT Htl HE HL Hown".
+    iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first set_solver.
+    iDestruct "Hown" as (l) "[EQ #Hshr]". iDestruct "EQ" as %[=->].
+     assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. (* set_solver needs some help. *)
+    iMod (copy_shr_acc with "LFT Hshr Htl Hκ") as (q') "(Htl & H↦ & Hcl)".
+    { set_solver. } { rewrite ->shr_locsE_shrN. set_solver. }
+    iDestruct "H↦" as (vl) "[>Hmt #Hown]". iModIntro. iExists _, _, _.
+    iSplit; first done. iFrame "∗#". iIntros "Hmt".
+    iMod ("Hcl" with "Htl [Hmt]") as "[$ Hκ]".
+    { iExists _. iFrame "∗#". }
+    iMod ("Hclose" with "Hκ") as "[$ $]". iExists _. auto.
   Qed.
 
-
 End typing.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index be284e13666cd036f7693c97b51b91e9875c9f2d..a55d5ee10ab60d9325ea51ac4ec88f00b4b6baee 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -163,14 +163,14 @@ Section sum.
       intros. apply @copy_persistent. edestruct nth_in_or_default as [| ->];
                                         [by eapply List.Forall_forall| apply _].
     - intros κ tid E F l q ? HF.
-      iIntros "#LFT #H [Htok1 Htok2] Htl".
+      iIntros "#LFT #H Htl [Htok1 Htok2]".
       setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
       iMod (frac_bor_acc with "LFT Hshr0 Htok1") as (q'1) "[>Hown Hclose]". set_solver.
       iAssert ((∃ vl, is_pad i tyl vl)%I) with "[#]" as %[vl Hpad].
       { iDestruct "Hown" as "[_ Hpad]". iDestruct "Hpad" as (vl) "[_ %]".
         eauto. }
-      iMod (@copy_shr_acc _ _ (nth i tyl ∅) with "LFT Hshr Htok2 Htl")
-        as (q'2) "(HownC & Htl & Hclose')"; try done.
+      iMod (@copy_shr_acc _ _ (nth i tyl ∅) with "LFT Hshr Htl Htok2")
+        as (q'2) "(Htl & HownC & Hclose')"; try done.
       { edestruct nth_in_or_default as [| ->]; last by apply _.
           by eapply List.Forall_forall. }
       { rewrite <-HF. simpl. rewrite <-union_subseteq_r.
@@ -187,12 +187,12 @@ Section sum.
       iDestruct "HownC" as "[HownC1 HownC2]". iDestruct "Hown" as "[Hown1 Hown2]".
       iExists q'. iModIntro. iSplitL "Hown1 HownC1".
       + iNext. iExists i. iFrame.
-      + iIntros "H Htl". iDestruct "H" as (i') "[>Hown1 HownC1]".
+      + iIntros "Htl H". iDestruct "H" as (i') "[>Hown1 HownC1]".
         iDestruct ("Htlclose" with "Htl") as "Htl".
         iDestruct (heap_mapsto_agree with "[Hown1 Hown2]") as "#Heq".
         { iDestruct "Hown1" as "[$ _]". iDestruct "Hown2" as "[$ _]". }
         iDestruct "Heq" as %[= ->%Z_of_nat_inj].
-        iMod ("Hclose'" with "[$HownC1 $HownC2] Htl") as "[? $]".
+        iMod ("Hclose'" with "Htl [$HownC1 $HownC2]") as "[$ ?]".
         iMod ("Hclose" with "[$Hown1 $Hown2]") as "$". by iFrame.
   Qed.
 
diff --git a/theories/typing/type.v b/theories/typing/type.v
index d62a06cf9076f7271c0cb4426a45868e6c721f10..51a4d8c963db81eb482d4af12806e6616a4d68b5 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -103,11 +103,11 @@ Section type.
     copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
     copy_shr_acc κ tid E F l q :
       lftE ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F →
-      lft_ctx -∗ t.(ty_shr) κ tid l -∗
-        q.[κ] -∗ na_own tid F ={E}=∗ ∃ q', ▷(l ↦∗{q'}: t.(ty_own) tid) ∗
-                                     na_own tid (F ∖ shr_locsE l t.(ty_size)) ∗
-         (▷l ↦∗{q'}: t.(ty_own) tid -∗ na_own tid (F ∖ shr_locsE l t.(ty_size))
-                                                    ={E}=∗ q.[κ] ∗ na_own tid F)
+      lft_ctx -∗ t.(ty_shr) κ tid l -∗ na_own tid F -∗ q.[κ] ={E}=∗
+         ∃ q', na_own tid (F ∖ shr_locsE l t.(ty_size)) ∗
+           ▷(l ↦∗{q'}: t.(ty_own) tid) ∗
+        (na_own tid (F ∖ shr_locsE l t.(ty_size)) -∗ ▷l ↦∗{q'}: t.(ty_own) tid
+                                    ={E}=∗ na_own tid F ∗ q.[κ])
   }.
   Global Existing Instances copy_persistent.
 
@@ -174,13 +174,13 @@ Section type.
 
   Global Program Instance ty_of_st_copy st : Copy (ty_of_st st).
   Next Obligation.
-    intros st κ tid E ? l q ? HF. iIntros "#LFT #Hshr Hlft Htok".
+    intros st κ tid E ? l q ? HF. iIntros "#LFT #Hshr Htok Hlft".
     iDestruct (na_own_acc with "Htok") as "[$ Htok]"; first set_solver+.
     iDestruct "Hshr" as (vl) "[Hf Hown]".
     iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
     iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
     - iNext. iExists _. by iFrame.
-    - iIntros "Hmt1 Htok2". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
+    - iIntros "Htok2 Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
       iDestruct ("Htok" with "Htok2") as "$".
       iAssert (▷ ⌜length vl = length vl'⌝)%I as ">%".
       { iNext. iDestruct (st_size_eq with "Hown") as %->.