diff --git a/theories/typing/own.v b/theories/typing/own.v
index 0e85a682e283b037267b84bf95510a2494c66cb6..4c5e65a2f64cbe8576a98d858b0da8d1c787660e 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -234,7 +234,7 @@ Section typing.
     iIntros ([[|l|]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
     iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iExists l, _, _. iSplitR; first done. 
-    unfold heap_pointsto_vec at 1. iSplitL; iFrame "∗#"; auto.
+    iFrame "∗#"; auto.
   Qed.
 
   Lemma read_own_move E L ty n :
@@ -245,7 +245,7 @@ Section typing.
     iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>%".
     iExists l, vl, _. iSplitR; first done. 
-    unfold heap_pointsto_vec. iSplitL "H↦"; iFrame "∗#"; auto.
+    iFrame; auto.
     by iIntros "!> $".
   Qed.