From e4c96015866317abecf20604839c0894c8ebc5d5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Jun 2016 13:45:40 +0200
Subject: [PATCH] =?UTF-8?q?Notations=20for=20X=20=E2=8A=86=20Y=20=E2=8A=86?=
 =?UTF-8?q?=20Z.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 prelude/base.v             | 5 +++++
 program_logic/invariants.v | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/prelude/base.v b/prelude/base.v
index 22752705f..bfcb09aed 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -637,6 +637,11 @@ Notation "(⊄)" := (λ X Y, X ⊄ Y) (only parsing) : C_scope.
 Notation "( X ⊄ )" := (λ Y, X ⊄ Y) (only parsing) : C_scope.
 Notation "( ⊄ X )" := (λ Y, Y ⊄ X) (only parsing) : C_scope.
 
+Notation "X ⊆ Y ⊆ Z" := (X ⊆ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : C_scope.
+Notation "X ⊆ Y ⊂ Z" := (X ⊆ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : C_scope.
+Notation "X ⊂ Y ⊆ Z" := (X ⊂ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : C_scope.
+Notation "X ⊂ Y ⊂ Z" := (X ⊂ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : C_scope.
+
 (** The class [Lexico A] is used for the lexicographic order on [A]. This order
 is used to create finite maps, finite sets, etc, and is typically different from
 the order [(⊆)]. *)
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index cb554fa42..3fb3ba674 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -34,7 +34,7 @@ Qed.
 (** Fairly explicit form of opening invariants *)
 Lemma inv_open E N P :
   nclose N ⊆ E →
-  inv N P ⊢ ∃ E', ■ (E ∖ nclose N ⊆ E' ∧ E' ⊆ E) ★
+  inv N P ⊢ ∃ E', ■ (E ∖ nclose N ⊆ E' ⊆ E) ★
                     |={E,E'}=> ▷ P ★ (▷ P ={E',E}=★ True).
 Proof.
   rewrite /inv. iIntros {?} "Hinv". iDestruct "Hinv" as {i} "[% #Hi]".
-- 
GitLab