diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index e63a253c79d28aabc8e5cff7d7feb9ef5ebf5bc4..99ceda8626896827b87f2f7b34229e80cc42767e 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -19,8 +19,7 @@ Section get_x.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret p).
     inv_vec p=>p. simpl_subst.
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|].
-      iIntros (p'); simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
     iApply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_delete; [solve_typing..|].
     iApply (type_jump [_]); solve_typing.
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 5b0d3bc1f1da47639d92492407d5cc548ae781de..be375087c75d1682b85e261b7c9a6e7eddf64c32 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -17,12 +17,12 @@ Section init_prod.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
       inv_vec p=>x y. simpl_subst.
-    iApply type_deref; [solve_typing..|apply read_own_move|done|]. iIntros (x'). simpl_subst.
-    iApply type_deref; [solve_typing..|apply read_own_move|done|]. iIntros (y'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (y'). simpl_subst.
     iApply (type_new_subtype (Π[uninit 1; uninit 1])); [solve_typing..|].
       iIntros (r). simpl_subst. unfold Z.to_nat, Pos.to_nat; simpl.
-    iApply (type_assign (own_ptr 2 (uninit 1))); [solve_typing..|by apply write_own|].
-    iApply type_assign; [solve_typing..|by apply write_own|].
+    iApply (type_assign (own_ptr 2 (uninit 1))); [solve_typing..|].
+    iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply (type_jump [_]); solve_typing.
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 6960ab838a64967486c1b99988fab21b7b6edeac..4c25cf38829e581859f9c41f9ea1d5b4c71f4da9 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -28,14 +28,14 @@ Section lazy_lft.
     iApply type_new; [solve_typing|]. iIntros (f). simpl_subst.
     iApply type_new; [solve_typing|]. iIntros (g). simpl_subst.
     iApply type_int. iIntros (v42). simpl_subst.
-    iApply type_assign; [solve_typing|by eapply write_own|].
-    iApply (type_assign _ (&shr{α}_)); [solve_typing..|by eapply write_own|].
-    iApply type_assign; [solve_typing|by eapply write_own|].
-    iApply type_deref; [solve_typing|apply: read_own_copy|done|]. iIntros (t0'). simpl_subst.
+    iApply type_assign; [solve_typing..|].
+    iApply (type_assign _ (&shr{α}_)); [solve_typing..|].
+    iApply type_assign; [solve_typing..|].
+    iApply type_deref; [solve_typing..|]. iIntros (t0'). simpl_subst.
     iApply type_letpath; [solve_typing|]. iIntros (dummy). simpl_subst.
     iApply type_int. iIntros (v23). simpl_subst.
-    iApply type_assign; [solve_typing|by eapply write_own|].
-    iApply (type_assign _ (&shr{α}int)); [solve_typing..|by eapply write_own|].
+    iApply type_assign; [solve_typing..|].
+    iApply (type_assign _ (&shr{α}int)); [solve_typing..|].
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_endlft; [solve_typing..|].
     iApply (type_delete (Π[&shr{_}_;&shr{_}_])%T); [solve_typing..|].
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 9ec1c0c88f25d79b30c8f21bea0b8a8d13ea865f..9d7a129778b8b222fe8e209806dc7c0f86fe3f6d 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -23,10 +23,10 @@ Section rebor.
        inv_vec p=>t1 t2. simpl_subst.
     iApply (type_newlft []). iIntros (α).
     iApply (type_letalloc_1 (&uniq{α}Π[int; int])); [solve_typing..|]. iIntros (x). simpl_subst.
-    iApply type_deref; [solve_typing|apply read_own_move|done|]. iIntros (x'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iApply (type_letpath (&uniq{α}int)); [solve_typing|]. iIntros (y). simpl_subst.
-    iApply (type_assign _ (&uniq{α}Π [int; int])); [solve_typing|by apply write_own|].
-    iApply type_deref; [solve_typing|apply: read_uniq; solve_typing|done|]. iIntros (y'). simpl_subst.
+    iApply (type_assign _ (&uniq{α}Π [int; int])); [solve_typing..|].
+    iApply type_deref; [solve_typing..|]. iIntros (y'). simpl_subst.
     iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_endlft.
     iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 78a3b34bb03cbbe912d21e8341e296fc7b5648b3..f1e7aaa443fdd1ca5991d043b96d1290a17dd313 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -16,8 +16,7 @@ Section unbox.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret b).
       inv_vec b=>b. simpl_subst.
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|].
-    iIntros (b'); simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (b'); simpl_subst.
     iApply type_deref_uniq_own; [solve_typing..|]. iIntros (bx); simpl_subst.
     iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/option.v b/theories/typing/option.v
index 7aea21c9fbdea20b00fc61908941eca7dcf5b5a1..279a0e79457bce404b93ac7a83eb93a0e42677c9 100644
--- a/theories/typing/option.v
+++ b/theories/typing/option.v
@@ -25,14 +25,13 @@ Section option.
       inv_vec p=>o. simpl_subst.
     iApply (type_cont [_] [] (λ r, [o ◁ _; r!!!0 ◁ _])%TC) ; [solve_typing..| |].
     - iIntros (k). simpl_subst.
-      iApply type_deref; [solve_typing|apply read_own_move|done|].
-        iIntros (o'). simpl_subst.
+      iApply type_deref; [solve_typing..|]. iIntros (o'). simpl_subst.
       iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
       iApply type_case_uniq; [solve_typing..|].
         constructor; last constructor; last constructor; left.
-      + iApply (type_sum_assign_unit [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|].
+      + iApply (type_sum_assign_unit [unit; &uniq{α}τ]%T); [solve_typing..|].
         iApply (type_jump [_]); solve_typing.
-      + iApply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|by apply write_own|].
+      + iApply (type_sum_assign [unit; &uniq{α}τ]%T); [solve_typing..|].
         iApply (type_jump [_]); solve_typing.
     - iIntros "/= !#". iIntros (k r). inv_vec r=>r. simpl_subst.
       iApply type_delete; [solve_typing..|].
@@ -57,8 +56,7 @@ Section option.
     iApply type_case_own; [solve_typing|]. constructor; last constructor; last constructor.
     + right. iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
-    + left. iApply type_letalloc_n; [solve_typing|by apply read_own_move|]. iIntros (r).
-        simpl_subst.
+    + left. iApply type_letalloc_n; [solve_typing..|]. iIntros (r). simpl_subst.
       iApply (type_delete (Π[uninit _;uninit _;uninit _])); [solve_typing..|].
       iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 25eba634ea8fad570bf9ac2019548fc6bd75a123..ffb893acd32b264f77622a08ac1dff5840528a32 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -298,7 +298,10 @@ Section typing.
   Qed.
 End typing.
 
-Hint Resolve own_mono' own_proper' : lrust_typing.
+Hint Resolve own_mono' own_proper' write_own read_own_copy : lrust_typing.
+(* By setting the priority high, we make sure copying is tryed before
+   moving. *)
+Hint Resolve read_own_move | 100 : lrust_typing.
 
 Hint Extern 100 (_ ≤ _) => simpl; lia : lrust_typing.
 Hint Extern 100 (@eq Z _ _) => simpl; lia : lrust_typing.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index bfb27a38dda5405bc9d607a92dfbfe25ec7b41df..b18f281951eaf2622dbac2bbd772d16f361e4b58 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -292,3 +292,5 @@ Section typing_rules.
     typed_body E L C T (p1 <-{n} !p2;; e).
   Proof. iIntros. by iApply type_seq; first eapply (type_memcpy_instr ty ty1 ty1'). Qed.
 End typing_rules.
+
+Hint Opaque typed_read typed_write : lrust_typing.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 678aeb85dbddceeb66eab7eff5b04920c07ad68e..2a1abdb433aafba85473faec86506b1732603b6c 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -90,4 +90,4 @@ Section typing.
   Qed.
 End typing.
 
-Hint Resolve shr_mono' shr_proper' : lrust_typing.
+Hint Resolve shr_mono' shr_proper' read_shr : lrust_typing.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 9c7f4cc02ecd47c1f8215097857a1aee91d52289..1537f6b34456c036b268a930ab04ca703f34883e 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -210,7 +210,7 @@ Section typing.
   Qed.
 End typing.
 
-Hint Resolve uniq_mono' uniq_proper' : lrust_typing.
+Hint Resolve uniq_mono' uniq_proper' write_uniq read_uniq : lrust_typing.
 Hint Resolve tctx_extract_hasty_reborrow | 10 : lrust_typing.
 Hint Resolve tctx_extract_hasty_share | 10 : lrust_typing.
 Hint Resolve tctx_extract_hasty_share_samelft | 9 : lrust_typing.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index a0063c1a4f4e91d6412ef21a36fc0b092040da9d..dcbc8431edb0c9147f19048fbaf03ac433204be9 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -130,7 +130,7 @@ Section typing.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_deref; [solve_typing|apply read_own_move|done|]. iIntros (x'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iApply type_letalloc_n; [solve_typing| |iIntros (r); simpl_subst].
     { apply (read_shr _ _ _ (cell ty)); solve_typing. }
     iApply type_delete; [solve_typing..|].
@@ -150,7 +150,8 @@ Section typing.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>c x. simpl_subst.
-    iApply type_deref; [solve_typing|exact: read_own_move|done|]. iIntros (c'); simpl_subst.
+    iApply type_deref; [solve_typing..|].
+    iIntros (c'); simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r); simpl_subst.
     (* Drop to Iris level. *)
     iIntros (tid qE) "#LFT Htl HE HL HC".
@@ -171,15 +172,12 @@ Section typing.
     iIntros "[Hr↦ Hc'↦]". wp_seq.
     iDestruct "Hx" as "[Hx↦ Hx†]". iDestruct "Hx↦" as (vx) "[Hx↦ Hxown]".
     rewrite Nat2Z.id. iDestruct (ty_size_eq with "Hxown") as "#%".
-    wp_apply (wp_memcpy with "[$Hc'↦ $Hx↦]").
-    { f_equal. done. }
-    { f_equal. done. }
+    wp_apply (wp_memcpy with "[$Hc'↦ $Hx↦]"); try by f_equal.
     iIntros "[Hc'↦ Hx↦]". wp_seq.
-    iMod ("Hclose" with "[Hc'↦ Hxown] Htl") as "[HE Htl]".
-    { iExists _. iFrame. }
+    iMod ("Hclose" with "[Hc'↦ Hxown] Htl") as "[HE Htl]"; first by auto with iFrame.
     (* Now go back to typing level. *)
     iApply (type_type _ _ _
-           [c ◁ box (uninit 1); #x ◁ box (uninit ty.(ty_size)); #r ◁ box ty]%TC
+           [c ◁ box (&shr{α} cell ty); #x ◁ box (uninit ty.(ty_size)); #r ◁ box ty]%TC
     with "[] LFT Htl [HE] HL HC"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
       iFrame "Hc". rewrite !tctx_hasty_val' //. iSplitL "Hx↦ Hx†".
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index 7cc4b5147952ae6f750ca4fbaa0329686f2a4bf0..8028c93efcdb6999e6d8c3ceaf0690304d9a2e2e 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -61,7 +61,7 @@ Section ref_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
+    iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
@@ -97,8 +97,8 @@ Section ref_functions.
         rewrite (comm Qp_plus) (assoc Qp_plus) Qp_div_2 (comm Qp_plus). auto. }
     iMod ("Hcloseβ" with "Hδ") as "Hβ". iMod ("Hcloseα1" with "[$H↦]") as "Hα1".
     iApply (type_type _ _ _
-        [ x ◁ box (uninit 1); #lr ◁ box(ref β ty)]%TC with "[] LFT Hna [Hα1 Hα2 Hβ] HL Hk");
-        first last.
+           [ x ◁ box (&shr{α} ref β ty); #lr ◁ box(ref β ty)]%TC
+        with "[] LFT Hna [Hα1 Hα2 Hβ] HL Hk"); first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       rewrite /= freeable_sz_full. iFrame. iExists _. iFrame. iExists _, _, _, _, _.
       iFrame "∗#". }
@@ -123,7 +123,7 @@ Section ref_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
+    iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
@@ -135,8 +135,8 @@ Section ref_functions.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. wp_let.
     iMod ("Hcloseα" with "[$H↦1 $H↦2]") as "Hα".
     iApply (type_type _ _ _
-        [ x ◁ box (uninit 1); #lv ◁ &shr{α}ty]%TC with "[] LFT Hna [Hα Hβ Hαβ] HL Hk");
-      first last.
+        [ x ◁ box (&shr{α} ref β ty); #lv ◁ &shr{α}ty]%TC
+        with "[] LFT Hna [Hα Hβ Hαβ] HL Hk"); first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "[] Hshr"). by iApply lft_incl_glb. }
     { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
@@ -262,15 +262,12 @@ Section ref_functions.
       rewrite (heap_mapsto_vec_cons _ _ _ [_]) !heap_mapsto_vec_singleton. iFrame.
       iExists ν, (q+qν')%Qp. eauto 10 with iFrame. }
     { rewrite /elctx_interp !big_sepL_cons /= -lft_tok_sep. iFrame. }
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|].
-      iIntros (x'). simpl_subst.
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|].
-      iIntros (f'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
     iApply type_letalloc_1; [solve_typing..|]. iIntros (x). simpl_subst.
     iApply (type_letcall); [simpl; solve_typing..|]. iIntros (r). simpl_subst.
-    iApply type_deref; [solve_typing|by eapply read_own_move|done|].
-      iIntros (r'). simpl_subst.
-    iApply type_assign; [solve_typing|by eapply write_own|].
+    iApply type_deref; [solve_typing..|]. iIntros (r'). simpl_subst.
+    iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply (type_jump []); solve_typing.
   Qed.
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index 7e8d244db936975e9ba2d7ed4f22f052cd1a9a05..af0545bc2e7b5ea949709e9b3f1b89366ccd13b1 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -98,8 +98,7 @@ Section refcell_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_deref; [solve_typing..|by eapply read_own_move|done|].
-      iIntros (x'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iIntros (tid qE) "#LFT Hna HE HL HC HT".
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|];  try iDestruct "Hx'" as "[]".
@@ -119,7 +118,7 @@ Section refcell_functions.
             with "[] LFT Hna HE HL HC [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iNext. iExists _. rewrite uninit_own. iFrame. }
-    iApply type_assign; [solve_typing..|exact: write_own|].
+    iApply type_assign; [solve_typing..|].
     iApply (type_jump [ #_]); solve_typing.
   Qed.
 
@@ -155,7 +154,7 @@ Section refcell_functions.
     { iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing. }
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply type_deref; [solve_typing..|apply read_own_copy, _|done|].
+    iApply type_deref; [solve_typing..|].
     iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
@@ -171,8 +170,7 @@ Section refcell_functions.
               with "[] LFT Hna >[Hclose Hβtok1 Hβtok2] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [unit; ref α ty]);
-        [solve_typing..|by eapply write_own|]; first last.
+      iApply (type_sum_assign_unit [unit; ref α ty]); [solve_typing..|]; first last.
       simpl. iApply (type_jump [_]); solve_typing.
     - wp_op. wp_write. wp_apply wp_new; [done..|].
       iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
@@ -224,8 +222,7 @@ Section refcell_functions.
         iFrame. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
         iApply lft_glb_mono. done. iApply lft_incl_refl. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_memcpy [unit; ref α ty]);
-        [solve_typing..|by eapply write_own|by eapply read_own_move|done|].
+      iApply (type_sum_memcpy [unit; ref α ty]); [solve_typing..|].
       simpl. iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
   Qed.
@@ -263,7 +260,7 @@ Section refcell_functions.
     { iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing. }
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply type_deref; [solve_typing..|apply read_own_copy, _|done|].
+    iApply type_deref; [solve_typing..|].
     iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
@@ -297,8 +294,7 @@ Section refcell_functions.
         iFrame. iExists _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
         iApply lft_glb_mono; first done. iApply lft_incl_refl. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_memcpy [unit; refmut α ty]);
-        [solve_typing..|by eapply write_own|by eapply read_own_move|done|].
+      iApply (type_sum_memcpy [unit; refmut α ty]); [solve_typing..|].
       simpl. iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
     - iMod ("Hclose'" with "[Hlx Hownst Hb] Hna") as "[Hβtok Hna]";
@@ -308,8 +304,7 @@ Section refcell_functions.
               with "[] LFT Hna >[Hclose Hβtok] HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
-      iApply (type_sum_assign_unit [unit; refmut α ty]);
-        [solve_typing..|by eapply write_own|].
+      iApply (type_sum_assign_unit [unit; refmut α ty]); [solve_typing..|].
       simpl. iApply (type_jump [_]); solve_typing.
   Qed.
 End refcell_functions.
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 06f36675a40d11419e58fca60adc1ad8134c6a20..d4b0c140c5659c06a72a64d471c0d23cc7a3753a 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -26,7 +26,7 @@ Section refmut_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
+    iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
@@ -41,7 +41,7 @@ Section refmut_functions.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_let.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
-    iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lv ◁ &shr{α}ty]%TC
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α} refmut β ty); #lv ◁ &shr{α}ty]%TC
             with "[] LFT Hna [Hα1 Hα2 Hβ Hαβ] HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "[] Hshr'"). iApply lft_incl_glb; first done.
@@ -68,7 +68,7 @@ Section refmut_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
+    iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']".
@@ -215,15 +215,12 @@ Section refmut_functions.
       rewrite (heap_mapsto_vec_cons _ _ _ [_]) !heap_mapsto_vec_singleton. iFrame.
       iExists ν. rewrite EQ1. eauto 10 with iFrame. }
     { rewrite /elctx_interp !big_sepL_cons /= -lft_tok_sep. iFrame. }
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|].
-      iIntros (x'). simpl_subst.
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|].
-       iIntros (f'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
     iApply type_letalloc_1; [solve_typing..|]. iIntros (x). simpl_subst.
     iApply (type_letcall); [simpl; solve_typing..|]. iIntros (r). simpl_subst.
-    iApply type_deref; [solve_typing|by eapply read_own_move|done|].
-      iIntros (r'). simpl_subst.
-    iApply type_assign; [solve_typing|by eapply write_own|].
+    iApply type_deref; [solve_typing..|]. iIntros (r'). simpl_subst.
+    iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply (type_jump []); solve_typing.
   Qed.
diff --git a/theories/typing/unsafe/rwlock/rwlock_code.v b/theories/typing/unsafe/rwlock/rwlock_code.v
index 9aa1f3504a273e2342c053e8e91875bced7c561c..f077e07228dd8038c8016b61f65e09a25f56d46b 100644
--- a/theories/typing/unsafe/rwlock/rwlock_code.v
+++ b/theories/typing/unsafe/rwlock/rwlock_code.v
@@ -96,8 +96,7 @@ Section rwlock_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_deref; [solve_typing..|by eapply read_own_move|done|].
-      iIntros (x'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iIntros (tid qE) "#LFT Hna HE HL HC HT".
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|];  try iDestruct "Hx'" as "[]".
@@ -117,7 +116,7 @@ Section rwlock_functions.
             with "[] LFT Hna HE HL HC [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iNext. iExists _. rewrite uninit_own. iFrame. }
-    iApply type_assign; [solve_typing..|exact: write_own|].
+    iApply type_assign; [solve_typing..|].
     iApply (type_jump [ #_]); solve_typing.
   Qed.
 
@@ -154,8 +153,7 @@ Section rwlock_functions.
     { iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing. }
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply type_deref; [solve_typing..|apply read_own_copy, _|done|].
-      iIntros (x'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iApply (type_cont [] [] (λ _, [x ◁ _; x' ◁ _; r ◁ _])%TC);
       [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
       simpl_subst.
@@ -177,7 +175,7 @@ Section rwlock_functions.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_assign_unit [unit; rwlockreadguard α ty]);
-        [solve_typing..|by eapply write_own|]; first last.
+        [solve_typing..|]; first last.
       simpl. iApply (type_jump [_]); solve_typing.
     - wp_op. wp_bind (CAS _ _ _).
       iMod (shr_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose']"; try done.
@@ -230,8 +228,7 @@ Section rwlock_functions.
           iExists _, _, _, _. iFrame "∗#". iApply ty_shr_mono; last done.
           iApply lft_glb_mono; first done. iApply lft_incl_refl. }
         { rewrite {1}/elctx_interp big_sepL_singleton //. }
-        iApply (type_sum_assign [unit; rwlockreadguard α ty]);
-          [solve_typing..|by eapply write_own|].
+        iApply (type_sum_assign [unit; rwlockreadguard α ty]); [solve_typing..|].
         simpl. iApply (type_jump [_]); solve_typing.
       + iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
         iMod ("Hclose'" with "[Hlx Hownst Hst]") as "Hβtok1"; first by iExists _; iFrame.
@@ -271,7 +268,7 @@ Section rwlock_functions.
       simpl_subst; last first.
     { iApply type_delete; [solve_typing..|]. iApply (type_jump [_]); solve_typing. }
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply type_deref; [solve_typing..|apply read_own_copy, _|done|].
+    iApply type_deref; [solve_typing..|].
     iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "(Hx & Hx' & Hr)". destruct x' as [[|lx|]|]; try done.
@@ -291,7 +288,7 @@ Section rwlock_functions.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_assign_unit [unit; rwlockwriteguard α ty]);
-        [solve_typing..|by eapply write_own|]; first last.
+        [solve_typing..|]; first last.
       rewrite /option /=. iApply (type_jump [_]); solve_typing.
     - iApply (wp_cas_int_suc with "Hlx"). done. iIntros "!> Hlx".
       iMod (own_update with "Hownst") as "[Hownst ?]".
@@ -305,8 +302,7 @@ Section rwlock_functions.
       { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
                 tctx_hasty_val' //. iFrame.  iExists _, _. iFrame "∗#". }
       { rewrite {1}/elctx_interp big_sepL_singleton //. }
-      iApply (type_sum_assign [unit; rwlockwriteguard α ty]);
-        [solve_typing..|by eapply write_own|].
+      iApply (type_sum_assign [unit; rwlockwriteguard α ty]); [solve_typing..|].
       simpl. iApply (type_jump [_]); solve_typing.
   Qed.
 End rwlock_functions.
diff --git a/theories/typing/unsafe/rwlock/rwlockreadguard_code.v b/theories/typing/unsafe/rwlock/rwlockreadguard_code.v
index 659d74d159c4c01b586bf242e22a32360c07df86..786d1abb82b91bf4156001d2ed2156e08a630dd3 100644
--- a/theories/typing/unsafe/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/unsafe/rwlock/rwlockreadguard_code.v
@@ -26,7 +26,7 @@ Section rwlockreadguard_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
+    iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
@@ -36,7 +36,8 @@ Section rwlockreadguard_functions.
     iMod (frac_bor_acc with "LFT Hfrac Hα") as (qlx') "[H↦ Hcloseα]". done.
     rewrite heap_mapsto_vec_singleton. wp_read. wp_op. wp_let.
     iMod ("Hcloseα" with "[$H↦]") as "Hα".
-    iApply (type_type _ _ _ [ x ◁ box (uninit 1); #(shift_loc l' 1) ◁ &shr{α}ty]%TC
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α} rwlockreadguard β ty);
+                              #(shift_loc l' 1) ◁ &shr{α}ty]%TC
       with "[] LFT Hna [Hα Hβ Hαβ] HL Hk"); first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "[] Hshr"). iApply lft_incl_glb. done.
@@ -65,7 +66,7 @@ Section rwlockreadguard_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|].
+    iApply type_deref; [solve_typing..|].
       iIntros (x'). simpl_subst.
     iApply (type_cont [] [] (λ _, [x ◁ _; x' ◁ _])%TC);
       [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
diff --git a/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v b/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
index b5a30a2855039d68745e1a0fff2588bb314000db..4cf42859f0a36baad5b30ddc51040fad8d1a61f0 100644
--- a/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
@@ -26,7 +26,7 @@ Section rwlockwriteguard_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
+    iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try done.
@@ -41,7 +41,8 @@ Section rwlockwriteguard_functions.
     iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_op. wp_let.
     iDestruct ("Hcloseβα2" with "Hα2β") as "[Hβ Hα2]".
     iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
-    iApply (type_type _ _ _ [ x ◁ box (uninit 1); #(shift_loc l' 1) ◁ &shr{α}ty]%TC
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α} rwlockwriteguard β ty);
+                              #(shift_loc l' 1) ◁ &shr{α}ty]%TC
             with "[] LFT Hna [Hα1 Hα2 Hβ Hαβ] HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "[] Hshr'"). iApply lft_incl_glb; first done.
@@ -68,7 +69,7 @@ Section rwlockwriteguard_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|]. iIntros (x').
+    iApply type_deref; [solve_typing..|]. iIntros (x').
     iIntros (tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iDestruct "HT" as "[Hx Hx']".
@@ -114,8 +115,7 @@ Section rwlockwriteguard_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_deref; [solve_typing..|by apply read_own_move|done|].
-      iIntros (x'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iIntros (tid qE) "#LFT Hna Hα HL Hk HT".
     rewrite {1}/elctx_interp big_sepL_singleton tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index beb525a3650bbde44a0251a28bf281d3ae865bfb..85b9c364d7d1dbb352c96c2382c6f34191844561 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -72,8 +72,7 @@ Section spawn.
   Proof. (* FIXME: typed_instruction_ty is not used for printing. *)
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret arg). inv_vec arg=>f env. simpl_subst.
-    iApply type_deref; [solve_typing..|exact: read_own_move|done|].
-    iIntros (f'). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
     iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _]%TC)
                      (λ j, [j ◁ join_handle retty]%TC)); try solve_typing; [|].
     { (* The core of the proof: showing that spawn is safe. *)
@@ -104,7 +103,7 @@ Section spawn.
         + rewrite !tctx_hasty_val. iApply @send_change_tid. done. }
     iIntros (v). simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply type_assign; [solve_typing..|exact: write_own|].
+    iApply type_assign; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply (type_jump [_]); solve_typing.
   Qed.
@@ -120,8 +119,7 @@ Section spawn.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret arg). inv_vec arg=>c. simpl_subst.
-    iApply type_deref; [solve_typing..|exact: read_own_move|done|].
-      iIntros (c'); simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (c'); simpl_subst.
     iApply (type_let _ _ _ _ ([c' ◁ _]%TC)
                              (λ r, [r ◁ box retty]%TC)); try solve_typing; [|].
     { iIntros (tid qE) "#LFT $ $ $".