diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index f8b6c3f17a0d60d12d874227a1ad47bca8ed9ef3..d84c70a2a801fd6108674498eb37bf145f0abbca 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -19,8 +19,8 @@ Section typing.
   Lemma type_bool (b : Datatypes.bool) E L :
     typed_instruction_ty E L [] #b bool.
   Proof.
-    iIntros (tid qE) "_ _ $ $ _". wp_value. rewrite tctx_interp_singleton.
-    iExists _. iSplitR; first done. iExists _. done.
+    iIntros (tid qE) "_ _ $ $ _". wp_value.
+    rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
   Qed.
 
   Lemma type_if E L C T e1 e2 p:
diff --git a/theories/typing/int.v b/theories/typing/int.v
index eb59fd32bc4d219c3ab242694e62db666fbaff18..fa0559634a6a924e1fd6751ac4094591a4903630 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -19,8 +19,8 @@ Section typing.
   Lemma type_int (z : Z) E L :
     typed_instruction_ty E L [] #z int.
   Proof.
-    iIntros (tid qE) "_ _ $ $ _". wp_value. rewrite tctx_interp_singleton.
-    iExists _. iSplitR; first done. iExists _. done.
+    iIntros (tid qE) "_ _ $ $ _". wp_value.
+    rewrite tctx_interp_singleton tctx_hasty_val. iExists _. done.
   Qed.
 
   Lemma type_plus E L p1 p2 :
@@ -32,7 +32,7 @@ Section typing.
     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.
+    wp_op. rewrite tctx_interp_singleton tctx_hasty_val' //.
     iExists _. done.
   Qed.
 
@@ -45,7 +45,7 @@ Section typing.
     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.
+    wp_op. rewrite tctx_interp_singleton tctx_hasty_val' //.
     iExists _. done.
   Qed.
 
@@ -58,8 +58,8 @@ Section typing.
     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);
+    wp_op; intros _; rewrite tctx_interp_singleton tctx_hasty_val' //;
       iExists _; done.
   Qed.
-  
+
 End typing.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 78138e0bd8ed85d3bef13d8e77e30afa9adb5649..198a55d017f561ffad2620c7117de57f6d130d56 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -140,15 +140,23 @@ Section typing.
 
   (** Typing *)
   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).
+    ty.(ty_size) = ty'.(ty_size) → typed_write 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†)".
     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 ">%". iModIntro. iExists _, _. iFrame "H↦".
-    iSplit; first by rewrite Hsz. iIntros (vl') "H↦ Hown' !>".
-    iExists _. iSplit; first done. rewrite Hsz. iFrame "H†".
-    iExists _. iFrame.
+    iSplit; first by rewrite Hsz. iIntros "Hown !>".
+    iExists _. iSplit; first done. rewrite Hsz. iFrame.
+  Qed.
+
+  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†)".
+    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.
   Qed.
 
   (* Old Typing *)
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 0479a70229c1fdde2035f92510f1d93cf1909704..d72cbc4b83ebfa91bd3662f8da0087c63a5b4346 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -46,12 +46,23 @@ Section typing.
   Global Arguments typed_instruction _ _ _ _%E _.
 
   (** Writing and Reading **)
-  Definition typed_writing (E : elctx) (L : llctx) (ty1 ty ty2 : type) : Prop :=
+  Definition typed_write (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}=∗
         ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌝ ∗ l ↦∗ vl ∗
-        ∀ vl', l ↦∗ vl' -∗ (ty.(ty_own) tid vl') ={F}=∗
-                  elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v].
+          (▷ l ↦∗: ty.(ty_own) tid ={F}=∗
+            elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]).
+
+  (* Technically speaking, we could remvoe the vl quantifiaction here and use
+     mapsto_pred instead (i.e., l ↦∗: ty.(ty_own) tid). However, that would
+     make work for some of the provers way harder, since they'd have to show
+     that nobody could possibly have changed the vl (because only half the
+     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}=∗
+        ∃ (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]).
 End typing.
 
 Notation typed_instruction_ty E L T1 e ty := (typed_instruction E L T1 e (λ v : val, [TCtx_hasty v ty])).
@@ -73,7 +84,7 @@ Section typing_rules.
   Qed.
   
   Lemma type_assign E L ty1 ty ty1' p1 p2 :
-    typed_writing E L ty1 ty ty1' →
+    typed_write E L ty1 ty ty1' →
     typed_instruction E L [TCtx_hasty p1 ty1; TCtx_hasty p2 ty] (p1 <- p2)
                       (λ _, [TCtx_hasty p1 ty1']).
   Proof.
@@ -87,8 +98,26 @@ Section typing_rules.
     rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
     rewrite heap_mapsto_vec_singleton. wp_write.
     rewrite -heap_mapsto_vec_singleton.
-    iMod ("Hclose" with "* Hl Hown2") as "($ & $ & Hown)".
+    iMod ("Hclose" with "* [Hl Hown2]") as "($ & $ & Hown)".
+    { iExists _. iFrame. }
     rewrite tctx_interp_singleton tctx_hasty_val' //.
   Qed.
 
+  Lemma type_deref E L ty1 ty ty1' p :
+    ty.(ty_size) = 1%nat → typed_read E L ty1 ty ty1' →
+    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.
+    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.
+    subst v. iAssert (▷⌜length vl = 1%nat⌝)%I with "[#]" as ">%".
+    { rewrite -Hsz. iApply ty_size_eq. done. }
+    destruct vl as [|v [|]]; try done.
+    rewrite heap_mapsto_vec_singleton. wp_read.
+    iMod ("Hclose" with "Hl") as "($ & $ & Hown2)".
+    rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
+    by iFrame.
+  Qed.
+
 End typing_rules.