diff --git a/prelude/base.v b/prelude/base.v
index 22752705fcfc727038368eb0053fb2d86e83e8c3..bfcb09aed3bd222aa10776452726f0578050b795 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 cb554fa42cd4bc33bd5cf9051c55429816e26512..3fb3ba6748b461a2969357512e961232af2c84cb 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]".