diff --git a/theories/base/at_cas.v b/theories/base/at_cas.v
index c6df76454968deff070614172f9a315986d119ad..c1b20371d17ee11f0095a37d8b2cae9cab1a0d0c 100644
--- a/theories/base/at_cas.v
+++ b/theories/base/at_cas.v
@@ -11,7 +11,7 @@ Lemma f_CAS `{fG : !foundationG Σ} π V l h (v_r v_w: Z):
         ∗ ( ⌜b = true⌝  ∗ ⌜v = v_r⌝
                       ∗ ⌜value_at h' V' (VInj v_w)⌝
                       ∗ ⌜h' ≡ {[VInj v_w, V']} ∪ h⌝
-                      ∗ ⌜h ⊥ {[VInj v_w, V']}⌝
+                      ∗ ⌜h ## {[VInj v_w, V']}⌝
                       ∗ ⌜init l h'⌝
                       ∗ ⌜adj_opt (V1 !! l) (V' !! l)⌝
                       ∗ ⌜no_adj_right l h V1⌝
diff --git a/theories/base/at_fai.v b/theories/base/at_fai.v
index 7c63dfe9d37a0236e156d7c5f113486b9055ae7c..1f3454957e4f4afee667eb62e99e7aebe2d0673e 100644
--- a/theories/base/at_fai.v
+++ b/theories/base/at_fai.v
@@ -11,7 +11,7 @@ Lemma f_FAI `{fG : !foundationG Σ} C π V l h:
             ∗ ⌜v' = (v + 1) `mod` Z.pos C⌝%Z
             ∗ ⌜value_at h' V' (VInj v')⌝
             ∗ ⌜h' ≡ {[VInj v', V']} ∪ h⌝
-            ∗ ⌜h ⊥ {[VInj v', V']}⌝
+            ∗ ⌜h ## {[VInj v', V']}⌝
             ∗ ⌜init l h'⌝
             ∗ ⌜adj_opt (V1 !! l) (V' !! l)⌝
             ∗ ⌜no_adj_right l h V1⌝ }}}.
diff --git a/theories/base/at_shared.v b/theories/base/at_shared.v
index 4f2aacce28c6492bfd5993b43e44f15346e4ae15..bdfdcbf9de60739ef8460947e40a678b15ba591d 100644
--- a/theories/base/at_shared.v
+++ b/theories/base/at_shared.v
@@ -22,7 +22,7 @@ Lemma write_at_update_hist ς ς' (V: View) h t l v (m: message)
         (VInj v, mview m) ∈ h'
         ∧ h' ≡ map_vt (hist_from (mem ς') l t)
         ∧ h' ≡ {[VInj v, mview m]} ∪ h
-        ∧ h ⊥ {[VInj v, mview m]}.
+        ∧ h ## {[VInj v, mview m]}.
 Proof.
   destruct Safe as [v' [V_l [Hv'1 Hv'2]]].
   assert (t ⊑ mtime m).
diff --git a/theories/base/at_write.v b/theories/base/at_write.v
index 626ec95f3738dbf98075ca38d9225086942d147e..eaf2569149e38ffa65a089385bab6b33cb7d2a9b 100644
--- a/theories/base/at_write.v
+++ b/theories/base/at_write.v
@@ -7,7 +7,7 @@ Lemma f_write_at `{fG : !foundationG Σ} π V_l l h v:
         ⌜V_l ⊑ V'⌝ ∗ Seen π V' 
          ∗ Hist l h' ∗ ⌜init_local h' V'⌝ ∗ ⌜init l h'⌝
          ∗ ⌜h' ≡ {[VInj v, V']} ∪ h⌝
-         ∗ ⌜h ⊥ {[VInj v, V']}⌝
+         ∗ ⌜h ## {[VInj v, V']}⌝
          ∗ ⌜value_at h' V' (VInj v)⌝}}}.
 Proof.
   iIntros (Φ) "(#I & Seen & Hist & %) Post".
diff --git a/theories/examples/circ_buffer.v b/theories/examples/circ_buffer.v
index e7380fccb0a00c6788d786e76db6754347daffa5..e25d4e1dc72dff85ca855d6fad863a0ea81d578e 100644
--- a/theories/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -101,7 +101,7 @@ Section CircBuffer.
       iIntros "Toks".
       rewrite /pToks_from /pTok. rewrite -own_op pair_op.
       rewrite !/op !/cmra_op /=.
-      case (decide ({[Pos.of_succ_nat i]} ⊥ coPset_from_ex (S i))) => [_|ND];
+      case (decide ({[Pos.of_succ_nat i]} ## coPset_from_ex (S i))) => [_|ND];
         last first.
         { exfalso. apply ND, coPset_from_disjoint. }
       iApply (own_mono with "Toks"). apply prod_included.
@@ -113,7 +113,7 @@ Section CircBuffer.
     Proof.
       iIntros "Toks".
       rewrite -own_op pair_op !/op !/cmra_op /=.
-      case (decide ({[Pos.of_succ_nat i]} ⊥ coPset_from_ex (S i))) => [_|ND];
+      case (decide ({[Pos.of_succ_nat i]} ## coPset_from_ex (S i))) => [_|ND];
         last first.
         { exfalso. apply ND, coPset_from_disjoint. }
       iApply (own_mono with "Toks"). apply prod_included.
@@ -126,9 +126,9 @@ Section CircBuffer.
     Proof.
       iIntros "Toks".
       rewrite -own_op pair_op !/op !/cmra_op /= /ucmra_op /=.
-      case (decide (coPset_from_ex i ⊥ ∅)) =>[_|ND]; last first.
+      case (decide (coPset_from_ex i ## ∅)) =>[_|ND]; last first.
         { exfalso. apply ND. set_solver+. }
-      case (decide (∅ ⊥ coPset_from_ex i)) =>[_|ND]; last first.
+      case (decide (∅ ## coPset_from_ex i)) =>[_|ND]; last first.
         { exfalso. apply ND. set_solver+. }
       iApply (own_mono with "Toks"). apply prod_included.
       rewrite /= !coPset_disj_included. set_solver+.
diff --git a/theories/examples/nat_tokens.v b/theories/examples/nat_tokens.v
index c1ffb8149f53e99f153b99970dc0d79a009331c1..c3611e7898620cfd9a5e839341a090039c9c59c8 100644
--- a/theories/examples/nat_tokens.v
+++ b/theories/examples/nat_tokens.v
@@ -36,7 +36,7 @@ Proof.
 Qed.
 
 Lemma coPset_from_disjoint i:
-  {[Pos.of_succ_nat i]} ⊥ coPset_from_ex (S i).
+  {[Pos.of_succ_nat i]} ## coPset_from_ex (S i).
 Proof.
   apply disjoint_singleton_l. rewrite coPset_from_ex_gt SuccNat2Pos.id_succ. lia.
 Qed.
@@ -57,7 +57,7 @@ Proof.
 Qed.
 
 Lemma coPset_of_gset_difference_union (X Y Z: gset positive)
-  (Disj: Y ⊥ Z) (Sub: Y ⊆ X):
+  (Disj: Y ## Z) (Sub: Y ⊆ X):
   coPset.of_gset (X ∖ Z) = coPset.of_gset (X ∖ (Y ∪ Z)) ∪ coPset.of_gset Y.
 Proof.
   apply leibniz_equiv. move => x.
@@ -71,14 +71,14 @@ Proof.
 Qed.
 
 Lemma coPset_of_gset_difference_disjoint (X Y Z: gset positive):
-  coPset.of_gset (X ∖ (Y ∪ Z)) ⊥ coPset.of_gset Y.
+  coPset.of_gset (X ∖ (Y ∪ Z)) ## coPset.of_gset Y.
 Proof.
   rewrite elem_of_disjoint.
   move => x. rewrite !coPset.elem_of_of_gset elem_of_difference elem_of_union.
   set_solver.
 Qed.
 
-Lemma coPset_of_gset_top_difference (X Y: gset positive) (Disj: X ⊥ Y):
+Lemma coPset_of_gset_top_difference (X Y: gset positive) (Disj: X ## Y):
   ⊤ ∖  coPset.of_gset X = (⊤ ∖  coPset.of_gset (Y ∪ X)) ∪ coPset.of_gset Y.
 Proof.
   apply leibniz_equiv. move => x.
@@ -90,7 +90,7 @@ Proof.
 Qed.
 
 Lemma coPset_of_gset_top_disjoint (X Y: gset positive):
-  (⊤ ∖  coPset.of_gset (Y ∪ X)) ⊥ coPset.of_gset Y.
+  (⊤ ∖  coPset.of_gset (Y ∪ X)) ## coPset.of_gset Y.
 Proof.
   rewrite elem_of_disjoint.
   move => x. rewrite elem_of_difference coPset_of_gset_union. set_solver.
diff --git a/theories/examples/rcu.v b/theories/examples/rcu.v
index f819593391821116f7a26dd6c05a96d543cf2437..b2add99bc4f3f9764d9766378bf2d813dae090af 100644
--- a/theories/examples/rcu.v
+++ b/theories/examples/rcu.v
@@ -353,7 +353,7 @@ Section RCU.
       ⊢ own γ {[ t := CoPset (⊤ ∖  coPset.of_gset Y) ]}
         ∗ own γ {[ t :=  CoPset $ coPset.of_gset (Y ∖ X) ]}.
     Proof.
-      have Hj: (X ⊥ Y ∖ X) by set_solver+.
+      have Hj: (X ## Y ∖ X) by set_solver+.
       rewrite (coPset_of_gset_top_difference _ _ Hj) -coPset_disj_union;
         last apply coPset_of_gset_top_disjoint.
       rewrite (union_comm_L (Y ∖ X)) -union_difference_L; last auto.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 5d2715bd3c2dae8256a6d3d17b6e6a9f28c0b593..4d3dca206224cc297134f0f9dcb6e16fc1d470b8 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -367,7 +367,7 @@ Section TicketLock.
     Proof.
       iIntros "Perms". rewrite -own_op pair_op.
       rewrite !/op /cmra_op /=.
-      case (decide ({[Pos.of_succ_nat t]} ⊥ coPset_from_ex (S t))) => [_|ND];
+      case (decide ({[Pos.of_succ_nat t]} ## coPset_from_ex (S t))) => [_|ND];
         last first.
         { exfalso. apply ND, coPset_from_disjoint. }
       iApply (own_mono with "Perms"). apply prod_included.
diff --git a/theories/gps/shared.v b/theories/gps/shared.v
index c27359ddacd634a0e67ca1799437e2bf94f592c7..d48730625dfb0f72c66d76769d8d72978e3862dc 100644
--- a/theories/gps/shared.v
+++ b/theories/gps/shared.v
@@ -189,7 +189,7 @@ Section Setup.
       Persistent (PrtSeen γ s V) := _.
 
     Lemma StateInjection_insert s v V h ζ
-          (Cons: Consistent ζ h) (SI: StateInjection ζ) (HDisj: h ⊥ {[VInj v,V]})
+          (Cons: Consistent ζ h) (SI: StateInjection ζ) (HDisj: h ## {[VInj v,V]})
       : StateInjection ({[s, (v, V)]} ∪ ζ).
     Proof.
       move => e1 e2 /elem_of_union [/elem_of_singleton ->| In1]
diff --git a/theories/lang/blocks.v b/theories/lang/blocks.v
index 2aec0036251c92aac81e39a0b3e9afeadc38dd53..922d36b3ece8927afa0ba0dc713c3ee5eef3eeb6 100644
--- a/theories/lang/blocks.v
+++ b/theories/lang/blocks.v
@@ -54,7 +54,7 @@ Section GHist.
 
   Lemma gblock_ends_ins_update x h p
         (OK: hTime_ok x ({[p]} ∪ h))
-        (Fresh: h ⊥ {[p]})
+        (Fresh: h ## {[p]})
   : gblock_ends_ins x h p (gblock_ends x h) (gblock_ends x ({[p]} ∪ h)).
   Proof.
     apply block_ends_ins.
diff --git a/theories/rsl/rsl.v b/theories/rsl/rsl.v
index a790e4a57bb7d5245e24236eba63b2e1f3eb7b89..0886f1b8be52f99b3ea886dd0ee1b3d810d99569 100644
--- a/theories/rsl/rsl.v
+++ b/theories/rsl/rsl.v
@@ -121,7 +121,7 @@ Instance InitRaw_persistent V jγ : Persistent (InitRaw V jγ) := _.
 
   Lemma big_sepS_gblock_ends_ins_update 
     l (h: History) p0 (Ψ: Val * View → iProp) 
-    (Disj: (h ⊥ {[p0]})%C)
+    (Disj: (h ## {[p0]})%C)
     (GB: gblock_ends_ins l h p0 (gblock_ends l h) (gblock_ends l ({[p0]} ∪ h)))
     : Ψ p0 ∗ ([∗ set] p ∈ gblock_ends l h, Ψ p)
       ⊢ ([∗ set] p ∈ gblock_ends l ({[p0]} ∪ h), Ψ p).
diff --git a/theories/rsl/rsl_sts.v b/theories/rsl/rsl_sts.v
index da40162ba0182eb6cc2a1c6a08293b6725895fe4..eca760c260e611fec5ee3dbeb93701e11dc96db2 100644
--- a/theories/rsl/rsl_sts.v
+++ b/theories/rsl/rsl_sts.v
@@ -295,15 +295,15 @@ Proof.
 Qed.
 
 (** Properties of split **)
-Lemma tok_disj_state_singleton s i: i ∈ rISet2 s → sts.tok s ⊥ {[Change i]}.
+Lemma tok_disj_state_singleton s i: i ∈ rISet2 s → sts.tok s ## {[Change i]}.
 Proof. abstract set_solver. Qed.
 
 Lemma state_ISet_split_token_disj_1 i1 i2 i s:
-  sts.tok (state_ISet_split i1 i2 i s) ⊥ {[Change i1]}.
+  sts.tok (state_ISet_split i1 i2 i s) ## {[Change i1]}.
 Proof. apply tok_disj_state_singleton. destruct s; abstract set_solver+. Qed.
 
 Lemma state_ISet_split_token_disj_2 i1 i2 i s:
-  sts.tok (state_ISet_split i1 i2 i s) ⊥ {[Change i2]}.
+  sts.tok (state_ISet_split i1 i2 i s) ## {[Change i2]}.
 Proof. apply tok_disj_state_singleton. destruct s; abstract set_solver+. Qed.
 
 Lemma state_ISet_split_included_1 i1 i2 i s:
diff --git a/theories/viewpred/viewpred.v b/theories/viewpred/viewpred.v
index 9a12a7753abd112422dc3fc2b53ac8f0d628ae13..8b1f587a74da24b802345ce29390744beb76b595 100644
--- a/theories/viewpred/viewpred.v
+++ b/theories/viewpred/viewpred.v
@@ -286,7 +286,7 @@ Notation "∀ x .. y , P" := (vPred_forall (λ x, .. (vPred_forall (λ y, P%VP))
 Notation "∃ x .. y , P" := (vPred_exists (λ x, .. (vPred_exists (λ y, P%VP)) ..)) : vPred_scope.
 Notation "P ∗ Q" := (vPred_sep P Q) : vPred_scope.
 Notation "x = y" := (vPred_pure (x%C%type = y%C%type)) : vPred_scope.
-Notation "x ⊥ y" := (vPred_pure (x%C%type ⊥ y%C%type)) : vPred_scope.
+Notation "x ## y" := (vPred_pure (x%C%type ## y%C%type)) : vPred_scope.
 Notation "'False'" := (vPred_pure False) : vPred_scope.
 Notation "'True'" := (vPred_pure True) : vPred_scope.
 Infix "∧" := vPred_and : vPred_scope.