From 3f1d431460b3e0b5aa99bbd21ca089d220dc66c3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 15 Mar 2017 17:26:52 +0100
Subject: [PATCH] Simplify a proof

---
 theories/typing/own.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/typing/own.v b/theories/typing/own.v
index 6abea77a..f5458177 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.
-- 
GitLab