diff --git a/algebra/upred.v b/algebra/upred.v
index 8f53aca1ead452fedac0021ca08195ebc3e2cb49..e0a9e313f742e61905f5463b5115a1cb5a02c0d8 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -276,6 +276,7 @@ Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
 Notation "■ φ" := (uPred_const φ%C%type)
   (at level 20, right associativity) : uPred_scope.
 Notation "x = y" := (uPred_const (x%C%type = y%C%type)) : uPred_scope.
+Notation "x ⊥ y" := (uPred_const (x%C%type ⊥ y%C%type)) : uPred_scope.
 Notation "'False'" := (uPred_const False) : uPred_scope.
 Notation "'True'" := (uPred_const True) : uPred_scope.
 Infix "∧" := uPred_and : uPred_scope.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index a74e0ad5f55bf5278e3b6056a811087be2fcff8c..9de604041ae5340936cbf77d52798e9918db850d 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -24,10 +24,10 @@ Definition lock_inv (γ : gname) (l : loc) (R : iProp) : iProp :=
   (∃ b : bool, l ↦ #b ★ if b then True else own γ (Excl ()) ★ R)%I.
 
 Definition is_lock (l : loc) (R : iProp) : iProp :=
-  (∃ N γ, ■ (heapN ⊥ N) ∧ heap_ctx heapN ∧ inv N (lock_inv γ l R))%I.
+  (∃ N γ, heapN ⊥ N ∧ heap_ctx heapN ∧ inv N (lock_inv γ l R))%I.
 
 Definition locked (l : loc) (R : iProp) : iProp :=
-  (∃ N γ, ■ (heapN ⊥ N) ∧ heap_ctx heapN ∧
+  (∃ N γ, heapN ⊥ N ∧ heap_ctx heapN ∧
           inv N (lock_inv γ l R) ∧ own γ (Excl ()))%I.
 
 Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 52208d3af21aa488e74f32fc9b8782a225fd7156..5172ea364f5e4599804d51b34e5ef8e3e7483c13 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -37,8 +37,8 @@ Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp :=
                    ∃ v, lv = InjRV v ★ (Ψ v ∨ own γ (Excl ()))))%I.
 
 Definition join_handle (l : loc) (Ψ : val → iProp) : iProp :=
-  (■ (heapN ⊥ N) ★ ∃ γ, heap_ctx heapN ★ own γ (Excl ()) ★
-                        inv N (spawn_inv γ l Ψ))%I.
+  (heapN ⊥ N ★ ∃ γ, heap_ctx heapN ★ own γ (Excl ()) ★
+                    inv N (spawn_inv γ l Ψ))%I.
 
 Typeclasses Opaque join_handle.