Fix broken proofs for improved iFrame ∃

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.