From 5df249005c6f8d906e28022a7c61beaa7578834d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 3 Oct 2020 14:58:54 +0200
Subject: [PATCH] Remove unused lemma.
---
theories/logatom/flat_combiner/misc.v | 14 --------------
1 file changed, 14 deletions(-)
diff --git a/theories/logatom/flat_combiner/misc.v b/theories/logatom/flat_combiner/misc.v
index fefa7acc..356c5b9a 100644
--- a/theories/logatom/flat_combiner/misc.v
+++ b/theories/logatom/flat_combiner/misc.v
@@ -29,20 +29,6 @@ Section excl.
Qed.
End excl.
-Section heap_extra.
- Context `{heapG Σ}.
-
- Lemma bogus_heap p (q1 q2: Qp) a b:
- ~((q1 + q2)%Qp ≤ 1%Qp)%Qc →
- p ↦{q1} a ∗ p ↦{q2} b ⊢ False.
- Proof.
- iIntros (?) "Hp".
- iDestruct "Hp" as "[Hl Hr]".
- iDestruct (@mapsto_valid_2 with "Hl Hr") as %H'. done.
- Qed.
-
-End heap_extra.
-
Section big_op_later.
Context {M : ucmraT}.
Context `{Countable K} {A : Type}.
--
GitLab