diff --git a/opam b/opam
index ed6e7f783cf2fecdf03f745607f7d2b06ad33e74..2241aec047d6bfbf1cc284aaf97094c0e31c8221 100644
--- a/opam
+++ b/opam
@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2020-03-18.6.d157edcc") | (= "dev") }
+  "coq-iris" { (= "dev.2020-03-21.0.ed3b52f9") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index c3c800273fb64179782f3f1c2734379fc360b1e0..1cdd3aabe3cd532b1e80ca160f1926b962a6f14a 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 484a81876a4c3f5bac973126a04ec513c86973d3..3ac859d671f7e23250a61825fc9dcd85918f2ef6 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -221,7 +221,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.
@@ -229,7 +230,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.
@@ -238,7 +240,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 1e0f46306df8791e08b97e32fd54966f40820b49..7892eb975c404f67b47079ade341c0e0153b6a2e 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -54,27 +54,41 @@ Section typing.
   Global Arguments typed_instruction _ _ _ _%E _.
 
   (** Writing and Reading **)
-  Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
+  Definition typed_write_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
     (□ ∀ 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) : iProp Σ :=
+  Definition typed_read_def (E : elctx) (L : llctx) (ty1 ty ty2 : type) : iProp Σ :=
     (□ ∀ 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)
@@ -196,6 +210,7 @@ Section typing_rules.
     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".
+    rewrite typed_write_eq in Hwrt.
     iMod (Hwrt with "[] LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
     subst v1. iDestruct (ty_size_eq with "Hown2") as "#Hsz". iDestruct "Hsz" as %Hsz.
     rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
@@ -221,6 +236,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").
     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.
     subst v. iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
@@ -253,6 +269,7 @@ Section typing_rules.
     iIntros (Φ) "(#LFT & #HE & Htl & [HL1 HL2] & [Hp1 Hp2]) HΦ".
     wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"). 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")
@@ -274,8 +291,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.
@@ -290,5 +305,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 127ecbf654fc234485c77cc5f7201efc5d92a90a..d61c770b6778dc271f07dbbbb73e0568662e70ad 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -153,6 +153,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"). 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]".
@@ -190,7 +191,8 @@ Section case.
   Proof.
     iIntros (Hty Hw tid) "#LFT #HE $ HL Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). 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.
     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' //.
@@ -224,13 +226,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"). 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] ->].
+    clear 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"). 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)"=>//=.
-    subst. assert (ty.(ty_size) ≤ length vl1).
+    clear Hr. subst. 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 e1290e814598cfb4be94bdb6b3b9beb716884d0b..a84b95b423ded0750fb579ce735420f19b16cda8 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -131,7 +131,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.
@@ -145,7 +145,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.