diff --git a/opam.pins b/opam.pins
index ad60b637b1252cfed2b814cde2069041ce0ecc3a..22cd46058e3d6684f434b070dd68ca6354d1d8b8 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 4e1bdcc778381975fbcef1c24736ec384c5ba661
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq c325f7a97464f0242e534938c5941a72c29452a2
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index a3ceea19afb4e70456334039c900d1af9ab6bd8d..cf803ad3d4bf217e7f238006009e529509c1e61c 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -200,19 +200,15 @@ Section code.
     iIntros (tid qE) "#LFT Hna HE HL Hk HT".
     rewrite (Nat2Z.id (S ty.(ty_size))) 2!tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "[Hrc [Hrcbox Hx]]". destruct x as [[|lx|]|]; try done.
-    iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[Hx↦ Hx]".
-    destruct rcbox as [[|lrcbox|]|]; try done. iDestruct "Hrcbox" as "[Hrcbox Hrcbox†]".
-    iDestruct "Hrcbox" as (vl') "Hrcbox". rewrite uninit_own.
-    iDestruct "Hrcbox" as "[>Hrcbox↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
-    rewrite heap_mapsto_vec_cons. iDestruct "Hrcbox↦" as "[Hrcbox↦0 Hrcbox↦1]".
-    destruct rc as [[|lrc|]|]; try done. iDestruct "Hrc" as "[Hrc Hrc†]".
-    iDestruct "Hrc" as (vl'') "Hrc". rewrite uninit_own.
-    iDestruct "Hrc" as "[>Hrc↦ >SZ]". destruct vl'' as [|]; iDestruct "SZ" as %[=].
-    destruct vl'' as [|]; last done. rewrite heap_mapsto_vec_singleton.
+    iDestruct "HT" as "[Hrc [Hrcbox Hx]]".
+    iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
+    iDestruct (ownptr_uninit_own with "Hrcbox") as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox.
+    inv_vec vlrcbox=>??. iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".
+    iDestruct (ownptr_uninit_own with "Hrc") as (lrc vlrc) "(% & Hrc↦ & Hrc†)". subst rc.
+    inv_vec vlrc=>?. rewrite heap_mapsto_vec_singleton.
     (* All right, we are done preparing our context. Let's get going. *)
     wp_op. rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
-    wp_apply (wp_memcpy with "[$Hrcbox↦1 $Hx↦]"); [done||lia..|].
+    wp_apply (wp_memcpy with "[$Hrcbox↦1 $Hx↦]"); [by auto using vec_to_list_length..|].
     iIntros "[Hrcbox↦1 Hx↦]". wp_seq. wp_op. rewrite shift_loc_0. wp_write.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lrc ◁ box (rc ty)]%TC
         with "[] LFT Hna HE HL Hk [-]"); last first.
@@ -247,10 +243,8 @@ Section code.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iIntros "[Hx [Hrc' Hrc2]]". rewrite [[x]]lock.
     destruct rc' as [[|lrc|]|]; try done. iDestruct "Hrc'" as (l') "[#Hlrc #Hshr]".
-    destruct rc2 as [[|lrc2|]|]; try done. iDestruct "Hrc2" as "[Hrc2 Hrc2†]".
-    iDestruct "Hrc2" as (vl) "[>Hrc2 >SZ]". rewrite uninit_own.
-    destruct vl as [|]; iDestruct "SZ" as %[=].
-    destruct vl as [|]; last done. rewrite heap_mapsto_vec_singleton.
+    iDestruct (ownptr_uninit_own with "Hrc2") as (lrc2 vlrc2) "(% & Hrc2 & Hrc2†)".
+    subst rc2. inv_vec vlrc2=>rc2. rewrite heap_mapsto_vec_singleton.
     (* All right, we are done preparing our context. Let's get going. *)
     rewrite {1}/elctx_interp big_sepL_singleton.
     iDestruct "HE" as "[Hα1 Hα2]". wp_bind (!_)%E.
@@ -309,11 +303,9 @@ Section code.
     iIntros (tid qE) "#LFT Hna HE HL Hk".
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
     iIntros "[Hrcx [Hrc' Hx]]". rewrite [[rcx]]lock.
-    destruct x as [[|x|]|]; try done. simpl of_val. (* TODO: simpl unfolds too much *)
-    iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[>Hx >SZ]".
-    rewrite uninit_own. destruct vl as [|]; iDestruct "SZ" as %[=].
-    destruct vl as [|]; last done. rewrite heap_mapsto_vec_singleton.
-    destruct rc' as [[|rc'|]|]; try done. simpl.
+    iDestruct (ownptr_uninit_own with "Hx") as (lrc2 vlrc2) "(% & Hx & Hx†)".
+    subst x. inv_vec vlrc2=>?. rewrite heap_mapsto_vec_singleton. 
+    destruct rc' as [[|rc'|]|]; try done. simpl of_val.
     iDestruct "Hrc'" as (l') "[#Hrc' #Hdelay]".
     (* All right, we are done preparing our context. Let's get going. *)
     rewrite {1}/elctx_interp big_sepL_singleton. iDestruct "HE" as "[Hα1 Hα2]". wp_bind (!_)%E.
@@ -324,9 +316,9 @@ Section code.
     iDestruct "Hproto" as (γ ν q'') "(#Hincl & #Hinv & #Hrctokb & #Hshr)". iModIntro.
     wp_op. wp_write.
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ rcx ◁ box (&shr{α} rc ty); #x ◁ box (&shr{α} ty)]%TC
+    iApply (type_type _ _ _ [ rcx ◁ box (&shr{α} rc ty); #lrc2 ◁ box (&shr{α} ty)]%TC
         with "[] LFT Hna [Hα1 Hα2] HL Hk [-]"); last first.
-    { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val !tctx_hasty_val' //.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame "Hrcx". iFrame "Hx†". iExists [_]. rewrite heap_mapsto_vec_singleton.
       iFrame "Hx". iNext. iApply ty_shr_mono; done. }
     { rewrite /elctx_interp big_sepL_singleton. iFrame. }
@@ -510,10 +502,9 @@ Section code.
     destruct rc' as [[|rc'|]|]; try done. rewrite [[rcx]]lock [[x]]lock.
     rewrite {1}/elctx_interp big_sepL_singleton.
     iMod (bor_acc_cons with "LFT Hrc' HE") as "[Hrc' Hclose1]"; first solve_ndisj.
-    iDestruct "Hrc'" as (vl) "[>Hrc' Hrcown]".
-    iDestruct (ty_size_eq with "Hrcown") as "#>%".
-    destruct vl as [|l vl]; first done. destruct vl; last done.
-    rewrite heap_mapsto_vec_singleton. wp_read. destruct l as [[|l|]|]; try done.
+    iDestruct (heap_mapsto_ty_own with "Hrc'") as (vl) "[>Hrc' Hrcown]".
+    inv_vec vl=>l. rewrite heap_mapsto_vec_singleton.
+    wp_read. destruct l as [[|l|]|]; try done.
     wp_let. wp_op. rewrite shift_loc_0.
     wp_apply (rc_check_unique with "[$Hna Hrcown]"); first done.
     { (* Boy this is silly... *) iDestruct "Hrcown" as "[(?&?&?)|?]"; last by iRight.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 5cac4cd58412846e7ae2aed41bf9a92bf3379d5e..5451b568d531047c288ae4de375477f0d6929ce3 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -28,14 +28,12 @@ Section refcell_functions.
     iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
-    iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[Hx↦ Hx]".
-    destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
-    iDestruct "Hr" as (vl') "Hr". rewrite uninit_own.
-    iDestruct "Hr" as "[Hr↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
-    rewrite heap_mapsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
+    iDestruct "HT" as "[Hr Hx]".
+    iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
+    iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
+    inv_vec vlr=>??. iDestruct (heap_mapsto_vec_cons with "Hr↦") as "[Hr↦0 Hr↦1]". wp_op.
     rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
-    wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [done||lia..|].
+    wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [by auto using vec_to_list_length..|].
     iIntros "[Hr↦1 Hx↦]". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (refcell ty)]%TC
         with "[] LFT Hna HE HL Hk [-]"); last first.
@@ -65,20 +63,20 @@ Section refcell_functions.
     iIntros (r tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
             tctx_interp_singleton !tctx_hasty_val.
-    iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
-    iDestruct "Hx" as "[Hx Hx†]".
-    iDestruct "Hx" as ([|[[]|]vl]) "[Hx↦ Hx]"; try iDestruct "Hx" as ">[]".
-    destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
-    iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_mapsto_vec_cons.
-    iDestruct "Hr" as "[Hr↦ >%]". iDestruct "Hx↦" as "[Hx↦0 Hx↦1]". wp_op.
-    iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
-    wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [done||lia..|].
+    iDestruct "HT" as "[Hr Hx]".
+    iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & >Hx↦ & Hx & Hx†)". subst x.
+    inv_vec vlx=>-[[|?|?]|????] vl; try iDestruct "Hx" as ">[]". simpl vec_to_list.
+    iDestruct "Hx" as "[>% Hx]".
+    iDestruct (heap_mapsto_vec_cons with "Hx↦") as "[Hx↦0 Hx↦1]".
+    iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
+    wp_op. wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [by auto using vec_to_list_length..|].
     iIntros "[Hr↦ Hx↦1]". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]%TC
         with "[] LFT Hna HE HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iSplitR "Hr↦ Hx".
-      - iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
+      - iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own. iFrame.
+        rewrite /= vec_to_list_length. auto.
       - iExists vl. iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index e53816252c2f4f46eb8a0a8040c99b8626acc1ba..6abea77a3de9160029f21e05d27b8790980ab127 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -174,16 +174,38 @@ Section box.
 
   Global Instance box_ne : NonExpansive box.
   Proof. apply type_contractive_ne, _. Qed.
+End box.
 
-(* For now, we use the instances inherited from own_ptr. *)
-(*  Global Instance box_send ty :
-    Send ty → Send (box ty).
-  Proof. apply _. Qed.
+Section util.
+  Context `{typeG Σ}.
 
-  Global Instance box_sync ty :
-    Sync ty → Sync (box ty).
-  Proof. apply _. Qed. *)
-End box.
+  Lemma ownptr_own n ty tid v :
+    (own_ptr n ty).(ty_own) tid [v] ⊣⊢
+       ∃ (l : loc) (vl : vec val ty.(ty_size)), ⌜v = #l⌝ ∗ ▷ l ↦∗ vl ∗ ▷ ty.(ty_own) tid vl ∗ ▷ freeable_sz n ty.(ty_size) l.
+  Proof.
+    iSplit.
+    - iIntros "Hown". destruct v as [[|l|]|]; try done.
+      iExists l. iDestruct "Hown" as "[Hown $]". rewrite heap_mapsto_ty_own.
+      iDestruct "Hown" as (vl) "[??]". eauto with iFrame.
+    - iIntros "Hown". iDestruct "Hown" as (l vl) "(% & ? & ? & ?)". subst v.
+      iFrame. iExists _. iFrame.
+  Qed.
+
+  Lemma ownptr_uninit_own n m tid v :
+    (own_ptr n (uninit m)).(ty_own) tid [v] ⊣⊢
+         ∃ (l : loc) (vl' : vec val m), ⌜v = #l⌝ ∗ ▷ l ↦∗ vl' ∗ ▷ freeable_sz n m l.
+  Proof.
+    rewrite ownptr_own. apply uPred.exist_proper=>l. iSplit.
+    (* FIXME: The goals here look rather confusing:  One cannot tell that we are looking at
+       a statement in Iris; the top-level → could just as well be a Coq implication. *)
+    - iIntros "H". iDestruct "H" as (vl) "(% & Hl & _ & $)". subst v.
+      rewrite -uPred.sep_exist_l. iSplit; first done.
+      iNext. eauto with iFrame.
+    - iIntros "H". iDestruct "H" as (vl) "(% & Hl & $)". subst v.
+      iExists vl. rewrite uninit_own vec_to_list_length.
+      eauto with iFrame.
+  Qed.
+End util.
 
 Section typing.
   Context `{typeG Σ}.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 6c34dabf165607c2aa39adfa6d96b137d8b9d276..bb4e356375148a25b07d814ee8b65be0f697067d 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -582,5 +582,19 @@ Section subtyping.
   Qed.
 End subtyping.
 
+Section type_util.
+  Context `{typeG Σ}.
+  
+  Lemma heap_mapsto_ty_own l ty tid :
+    l ↦∗: ty_own ty tid ⊣⊢ ∃ (vl : vec val ty.(ty_size)), l ↦∗ vl ∗ ty_own ty tid vl.
+  Proof.
+    iSplit.
+    - iIntros "H". iDestruct "H" as (vl) "[Hl Hown]".
+      iDestruct (ty_size_eq with "Hown") as %<-.
+      iExists (list_to_vec vl). rewrite vec_to_list_of_list. iFrame.
+    - iIntros "H". iDestruct "H" as (vl) "[Hl Hown]". eauto with iFrame.
+  Qed.
+End type_util.
+
 Hint Resolve subtype_refl eqtype_refl : lrust_typing.
 Hint Opaque subtype eqtype : lrust_typing.