diff --git a/theories/typing/own.v b/theories/typing/own.v
index 6abea77a3de9160029f21e05d27b8790980ab127..f5458177e1f6b450659092b14b6107f5fc2bbb0b 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -199,8 +199,7 @@ Section util.
     (* 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.
+      iExists vl. iSplit; done.
     - iIntros "H". iDestruct "H" as (vl) "(% & Hl & $)". subst v.
       iExists vl. rewrite uninit_own vec_to_list_length.
       eauto with iFrame.