From 0bc19271ead6c9b7a440db6716db2fec7dc93ac5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 6 Feb 2020 18:03:13 +0100
Subject: [PATCH] remove an assumption we no longer need

---
 theories/bi/lib/counterexamples.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index dd61261c9..cbf04fde4 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -299,8 +299,6 @@ Module linear2. Section linear2.
     fupd E E (∃ γ, ∀ P, ▷ P -∗ fupd E E (cinv γ P ∗ cinv_own γ))%I.
   Hypothesis cinv_access : ∀ P γ,
     cinv γ P -∗ cinv_own γ -∗ fupd M1 M0 (▷ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 emp)).
-  Hypothesis cinv_own_excl : ∀ E γ,
-    ▷ cinv_own γ -∗ ▷ cinv_own γ -∗ fupd E E False.
 
   (** Some general lemmas and proof mode compatibility. *)
   Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2).
-- 
GitLab