From c3c91b70a6db8a4aaf5a9150290c09dd4a82c231 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 6 Feb 2020 17:58:01 +0100
Subject: [PATCH] simplify proof considerably

---
 theories/bi/lib/counterexamples.v | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index 14f007b4e..dd61261c9 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -325,12 +325,8 @@ Module linear2. Section linear2.
   Proof.
     iIntros "HP".
     iMod cinv_alloc as (γ) "Hmkinv".
-    set (INV := (P ∨ cinv_own γ ∗ P)%I).
-    iMod ("Hmkinv" $! INV with "[HP]") as "(Hinv & Htok)".
-    { iLeft. done. }
-    iMod (cinv_access with "Hinv Htok") as "([HP|Hinv] & Htok & Hclose)"; last first.
-    { iDestruct "Hinv" as "(Htok' & ?)".
-      iMod (cinv_own_excl with "Htok Htok'") as "[]". }
-    iApply "Hclose". iNext. iRight. iFrame.
+    iMod ("Hmkinv" $! True%I with "[//]") as "[Hinv Htok]".
+    iMod (cinv_access with "Hinv Htok") as "(Htrue & Htok & Hclose)".
+    iApply "Hclose". done.
   Qed.
 End linear2. End linear2.
-- 
GitLab