diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index f76926ac34a251f04b0041703e221d372485ea06..352f6dc95edacd556bbd9ed3607283186b4494ef 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -168,7 +168,9 @@ Section typing.
       iIntros (α ϝ ret arg). inv_vec arg=>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. }
+    { rewrite typed_read_eq.
+      have Hrd := (read_shr _ _ _ (cell ty)). rewrite typed_read_eq in Hrd.
+      apply Hrd; solve_typing. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index cfad9eb1059c9764de8e91dbcdcb37be8d559aed..3372eab6ff115d7d83ac1d69b166e49f3c9ce79c 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -222,7 +222,8 @@ Section typing.
   Lemma write_own {E L} ty ty' n :
     ty.(ty_size) = ty'.(ty_size) → ⊢ typed_write E L (own_ptr n ty') ty (own_ptr n ty).
   Proof.
-    iIntros (Hsz) "!#". iIntros ([[]|] tid F qL ?) "_ _ $ Hown"; try done.
+    rewrite typed_write_eq. iIntros (Hsz) "!#".
+    iIntros ([[]|] tid F qL ?) "_ _ $ Hown"; try done.
     rewrite /= Hsz. iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>%". iExists _, _. iFrame "H↦". auto.
   Qed.
@@ -230,7 +231,8 @@ Section typing.
   Lemma read_own_copy E L ty n :
     Copy ty → ⊢ typed_read E L (own_ptr n ty) ty (own_ptr n ty).
   Proof.
-    iIntros (Hsz) "!#". iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
+    rewrite typed_read_eq. iIntros (Hsz) "!#".
+    iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
     iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iExists l, _, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !>".
     iExists _. auto.
@@ -239,7 +241,8 @@ Section typing.
   Lemma read_own_move E L ty n :
     ⊢ typed_read E L (own_ptr n ty) ty (own_ptr n $ uninit ty.(ty_size)).
   Proof.
-    iAlways. iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
+    rewrite typed_read_eq. iAlways.
+    iIntros ([[]|] tid F qL ?) "_ _ $ $ Hown"; try done.
     iDestruct "Hown" as "[H↦ H†]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>%".
     iExists l, vl, _. iFrame "∗#". iSplitR; first done. iIntros "!> Hl !> !>".
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 9f2751167d374b23346ccd67dcda98595783e7eb..b7caa3674f2834773a47c28b914f37ad41b2d36b 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -57,27 +57,41 @@ Section typing.
   Global Arguments typed_instruction _ _ _ _%E _.
 
   (** Writing and Reading **)
-  Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : vPropI Σ :=
+  Definition typed_write_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : vPropI Σ :=
     (□ ∀ v tid F qL, ⌜lftE ∪ (↑lrustN) ⊆ F⌝ →
       ⎡lft_ctx⎤ -∗ elctx_interp E -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
         ∃ (l : loc) vl, ⌜length vl = ty.(ty_size) ∧ v = #l⌝ ∗ l ↦∗ vl ∗
           (▷ l ↦∗: ty.(ty_own) tid ={F}=∗
             llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
+  Definition typed_write_aux : seal (@typed_write_def). by eexists. Qed.
+  Definition typed_write := typed_write_aux.(unseal).
+  Definition typed_write_eq : @typed_write = @typed_write_def := typed_write_aux.(seal_eq).
   Global Arguments typed_write _ _ _%T _%T _%T.
 
+  Global Instance typed_write_persistent (E : elctx) (L : llctx) (ty1 ty ty2 : type) :
+    Persistent (typed_write E L ty1 ty ty2).
+  Proof. rewrite typed_write_eq. apply _. Qed.
+
   (* 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) : vPropI Σ :=
+  Definition typed_read_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : vPropI Σ :=
     (□ ∀ v tid F qL, ⌜lftE ∪ ↑lrustN ⊆ F⌝ →
       ⎡lft_ctx⎤ -∗ elctx_interp E -∗ na_own tid F -∗
       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}=∗ na_own tid F ∗
                               llctx_interp L qL ∗ ty2.(ty_own) tid [v]))%I.
+  Definition typed_read_aux : seal (@typed_read_def). by eexists. Qed.
+  Definition typed_read := typed_read_aux.(unseal).
+  Definition typed_read_eq : @typed_read = @typed_read_def := typed_read_aux.(seal_eq).
   Global Arguments typed_read _ _ _%T _%T _%T.
+
+  Global Instance typed_read_persistent (E : elctx) (L : llctx) (ty1 ty ty2 : type) :
+    Persistent (typed_read E L ty1 ty ty2).
+  Proof. rewrite typed_read_eq. apply _. Qed.
 End typing.
 
 Definition typed_instruction_ty `{!typeG Σ} (E : elctx) (L : llctx) (T : tctx)
@@ -199,6 +213,7 @@ Section typing_rules.
     rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
     wp_bind p1. iApply (wp_hasty with "Hp1"); [done|]. iIntros (v1) "% Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"); [done|]. iIntros (v2) "_ Hown2".
+    rewrite typed_write_eq in Hwrt.
     iMod (Hwrt with "[] LFT HE HL Hown1") as (l vl [?[= ->]]) "(Hl & Hclose)"; first done.
     iDestruct (ty_size_eq with "Hown2") as "#Hsz". iDestruct "Hsz" as %Hsz.
     rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
@@ -224,6 +239,7 @@ Section typing_rules.
     iIntros (Hsz Hread tid) "#LFT #HE Htl HL Hp".
     rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp"); [done|].
     iIntros (v) "% Hown".
+    rewrite typed_read_eq in Hread.
     iMod (Hread with "[] LFT HE Htl HL Hown") as
         (l vl q [= ->]) "(Hl & Hown & Hclose)"; first done.
     iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
@@ -256,6 +272,7 @@ Section typing_rules.
     iIntros (Φ) "(#LFT & #HE & Htl & [HL1 HL2] & [Hp1 Hp2]) HΦ".
     wp_bind p1. iApply (wp_hasty with "Hp1"); [done|]. iIntros (v1) "% Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"); [done|]. iIntros (v2) "% Hown2".
+    rewrite typed_write_eq typed_read_eq.
     iMod ("Hwrt" with "[] LFT HE HL1 Hown1")
       as (l1 vl1 [?[= ->]]) "(Hl1 & Hcl1)"; first done.
     iMod ("Hread" with "[] LFT HE Htl HL2 Hown2")
@@ -277,8 +294,6 @@ Section typing_rules.
   Proof.
     iIntros (Hsz Hwrt Hread tid) "#LFT #HE Htl HL HT".
     iApply (type_memcpy_iris with "[] [] [$LFT $Htl $HE $HL HT]"); try done.
-    { iApply Hwrt. }
-    { iApply Hread. }
     { by rewrite tctx_interp_cons tctx_interp_singleton. }
     rewrite tctx_interp_cons tctx_interp_singleton. auto.
   Qed.
@@ -293,5 +308,3 @@ 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 b866efaf24206e3f30774df589945ec786fb48c1..cf899f62b334f43b7c45a3458569cec94193e526 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -84,7 +84,7 @@ Section typing.
   Lemma read_shr E L κ ty :
     Copy ty → lctx_lft_alive E L κ → ⊢ typed_read E L (&shr{κ}ty) ty (&shr{κ}ty).
   Proof.
-    iIntros (Hcopy Halive) "!#".
+    rewrite typed_read_eq. iIntros (Hcopy Halive) "!#".
     iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL #Hshr"; try done.
     iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first solve_ndisj.
     iMod (copy_shr_acc with "LFT Hshr Htl Hκ") as (q') "(Htl & H↦ & Hcl)"; first solve_ndisj.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 7de06ac50111453bae22235c292f8cdc6a301b2d..6e3582194ceed7cbae4cea4e89ae6c6733e166a6 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -154,6 +154,7 @@ Section case.
     iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
     iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
     iApply (wp_hasty with "Hp1"); [done|]. iIntros (v1 Hv1) "Hty1".
+    rewrite typed_write_eq in Hw.
     iMod (Hw with "[] LFT HE HL Hty1") as (l vl) "(H & H↦ & Hw)"=>//=.
     destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] [= ->]].
     rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[H↦0 H↦vl]".
@@ -191,7 +192,9 @@ Section case.
   Proof.
     iIntros (Hty Hw tid) "#LFT #HE $ HL Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"); [done|]. iIntros (v Hv) "Hty".
-    iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
+    rewrite typed_write_eq in Hw.
+    iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)"; first done.
+    clear Hw.
     simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] [= ->]].
     rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl]".
     wp_write. rewrite tctx_interp_singleton tctx_hasty_val' //.
@@ -225,13 +228,15 @@ Section case.
     iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
     iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
     iApply (wp_hasty with "Hp1"); [done|]. iIntros (v1 Hv1) "Hty1".
+    rewrite typed_write_eq in Hw.
     iMod (Hw with "[] LFT HE HL1 Hty1") as (l1 vl1) "(H & H↦ & Hw)"=>//=.
     destruct vl1 as [|? vl1]; iDestruct "H" as %[[= Hlen] [=->]].
     rewrite heap_mapsto_vec_cons -wp_fupd. iDestruct "H↦" as "[H↦0 H↦vl1]". wp_write.
     wp_bind p1. iApply (wp_wand with "[]"); first by iApply (wp_eval_path). iIntros (? ->).
     wp_op. wp_bind p2. iApply (wp_hasty with "Hp2"); [done|]. iIntros (v2 Hv2) "Hty2".
+    rewrite typed_read_eq in Hr.
     iMod (Hr with "[] LFT HE Htl HL2 Hty2") as (l2 vl2 q [= ->]) "(H↦2 & Hty & Hr)"=>//=.
-    assert (ty.(ty_size) ≤ length vl1).
+    clear Hr. assert (ty.(ty_size) ≤ length vl1).
     { revert i Hty. rewrite Hlen. clear. induction tyl=>//= -[|i] /=.
       - intros [= ->]. lia.
       - specialize (IHtyl i). intuition lia. }
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 0496a9e79c21bef5a6fa5b7fd12c3319fd0afee6..522d5d808f24e53f727d0c5e2832b9062887916b 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -130,7 +130,7 @@ Section typing.
   Lemma read_uniq E L κ ty :
     Copy ty → lctx_lft_alive E L κ → ⊢ typed_read E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
-    iIntros (Hcopy Halive) "!#".
+    rewrite typed_read_eq. iIntros (Hcopy Halive) "!#".
     iIntros ([[]|] tid F qL ?) "#LFT #HE Htl HL Hown"; try done.
     iMod (Halive with "HE HL") as (q) "[Hκ Hclose]"; first solve_ndisj.
     iMod (bor_acc with "LFT Hown Hκ") as "[H↦ Hclose']"; first solve_ndisj.
@@ -144,7 +144,7 @@ Section typing.
   Lemma write_uniq E L κ ty :
     lctx_lft_alive E L κ → ⊢ typed_write E L (&uniq{κ}ty) ty (&uniq{κ}ty).
   Proof.
-    iIntros (Halive) "!#".
+    rewrite typed_write_eq. iIntros (Halive) "!#".
     iIntros ([[]|] tid F qL ?) "#LFT HE HL Hown"; try done.
     iMod (Halive with "HE HL") as (q) "[Htok Hclose]"; first solve_ndisj.
     iMod (bor_acc with "LFT Hown Htok") as "[H↦ Hclose']"; first solve_ndisj.