From 4b5d254e8f78145735d6f03a507c6f3214cad89e Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 27 Oct 2017 14:20:34 +0200
Subject: [PATCH] =?UTF-8?q?Notation=20for=20disjointness:=20replace=20?=
 =?UTF-8?q?=E2=8A=A5=20with=20##,=20so=20that=20=E2=8A=A5=20can=20be=20use?=
 =?UTF-8?q?d=20for=20bottom.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base.v            |  62 +++++++-------
 theories/collections.v     |  38 ++++-----
 theories/fin_collections.v |   2 +-
 theories/fin_map_dom.v     |   6 +-
 theories/fin_maps.v        | 166 ++++++++++++++++++-------------------
 5 files changed, 137 insertions(+), 137 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index f0964e3c..59615541 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -660,7 +660,7 @@ Arguments sig_map _ _ _ _ _ _ !_ / : assert.
 (** We define operational type classes for the traditional operations and
 relations on collections: the empty collection [∅], the union [(∪)],
 intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
-[(⊆)] and element of [(∈)] relation, and disjointess [(⊥)]. *)
+[(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
 Class Empty A := empty: A.
 Hint Mode Empty ! : typeclass_instances.
 Notation "∅" := empty : C_scope.
@@ -779,56 +779,56 @@ Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : C_scope.
 Notation "(∉ X )" := (λ x, x ∉ X) (only parsing) : C_scope.
 
 Class Disjoint A := disjoint : A → A → Prop.
-Hint Mode Disjoint ! : typeclass_instances.
+ Hint Mode Disjoint ! : typeclass_instances.
 Instance: Params (@disjoint) 2.
-Infix "⊥" := disjoint (at level 70) : C_scope.
-Notation "(⊥)" := disjoint (only parsing) : C_scope.
-Notation "( X ⊥.)" := (disjoint X) (only parsing) : C_scope.
-Notation "(.⊥ X )" := (λ Y, Y ⊥ X) (only parsing) : C_scope.
-Infix "⊥*" := (Forall2 (⊥)) (at level 70) : C_scope.
-Notation "(⊥*)" := (Forall2 (⊥)) (only parsing) : C_scope.
-Infix "⊥**" := (Forall2 (⊥*)) (at level 70) : C_scope.
-Infix "⊥1*" := (Forall2 (λ p q, p.1 ⊥ q.1)) (at level 70) : C_scope.
-Infix "⊥2*" := (Forall2 (λ p q, p.2 ⊥ q.2)) (at level 70) : C_scope.
-Infix "⊥1**" := (Forall2 (λ p q, p.1 ⊥* q.1)) (at level 70) : C_scope.
-Infix "⊥2**" := (Forall2 (λ p q, p.2 ⊥* q.2)) (at level 70) : C_scope.
-Hint Extern 0 (_ ⊥ _) => symmetry; eassumption.
-Hint Extern 0 (_ ⊥* _) => symmetry; eassumption.
+Infix "##" := disjoint (at level 70) : C_scope.
+Notation "(##)" := disjoint (only parsing) : C_scope.
+Notation "( X ##.)" := (disjoint X) (only parsing) : C_scope.
+Notation "(.## X )" := (λ Y, Y ## X) (only parsing) : C_scope.
+Infix "##*" := (Forall2 (##)) (at level 70) : C_scope.
+Notation "(##*)" := (Forall2 (##)) (only parsing) : C_scope.
+Infix "##**" := (Forall2 (##*)) (at level 70) : C_scope.
+Infix "##1*" := (Forall2 (λ p q, p.1 ## q.1)) (at level 70) : C_scope.
+Infix "##2*" := (Forall2 (λ p q, p.2 ## q.2)) (at level 70) : C_scope.
+Infix "##1**" := (Forall2 (λ p q, p.1 ##* q.1)) (at level 70) : C_scope.
+Infix "##2**" := (Forall2 (λ p q, p.2 ##* q.2)) (at level 70) : C_scope.
+Hint Extern 0 (_ ## _) => symmetry; eassumption.
+Hint Extern 0 (_ ##* _) => symmetry; eassumption.
 
 Class DisjointE E A := disjointE : E → A → A → Prop.
 Hint Mode DisjointE - ! : typeclass_instances.
 Instance: Params (@disjointE) 4.
-Notation "X ⊥{ Γ } Y" := (disjointE Γ X Y)
-  (at level 70, format "X  ⊥{ Γ }  Y") : C_scope.
-Notation "(⊥{ Γ } )" := (disjointE Γ) (only parsing, Γ at level 1) : C_scope.
-Notation "Xs ⊥{ Γ }* Ys" := (Forall2 (⊥{Γ}) Xs Ys)
-  (at level 70, format "Xs  ⊥{ Γ }*  Ys") : C_scope.
-Notation "(⊥{ Γ }* )" := (Forall2 (⊥{Γ}))
+Notation "X ##{ Γ } Y" := (disjointE Γ X Y)
+  (at level 70, format "X  ##{ Γ }  Y") : C_scope.
+Notation "(##{ Γ } )" := (disjointE Γ) (only parsing, Γ at level 1) : C_scope.
+Notation "Xs ##{ Γ }* Ys" := (Forall2 (##{Γ}) Xs Ys)
+  (at level 70, format "Xs  ##{ Γ }*  Ys") : C_scope.
+Notation "(##{ Γ }* )" := (Forall2 (##{Γ}))
   (only parsing, Γ at level 1) : C_scope.
-Notation "X ⊥{ Γ1 , Γ2 , .. , Γ3 } Y" := (disjoint (pair .. (Γ1, Γ2) .. Γ3) X Y)
-  (at level 70, format "X  ⊥{ Γ1 , Γ2 , .. , Γ3 }  Y") : C_scope.
-Notation "Xs ⊥{ Γ1 , Γ2 , .. , Γ3 }* Ys" :=
+Notation "X ##{ Γ1 , Γ2 , .. , Γ3 } Y" := (disjoint (pair .. (Γ1, Γ2) .. Γ3) X Y)
+  (at level 70, format "X  ##{ Γ1 , Γ2 , .. , Γ3 }  Y") : C_scope.
+Notation "Xs ##{ Γ1 , Γ2 , .. , Γ3 }* Ys" :=
   (Forall2 (disjoint (pair .. (Γ1, Γ2) .. Γ3)) Xs Ys)
-  (at level 70, format "Xs  ⊥{ Γ1 ,  Γ2 , .. , Γ3 }*  Ys") : C_scope.
-Hint Extern 0 (_ ⊥{_} _) => symmetry; eassumption.
+  (at level 70, format "Xs  ##{ Γ1 ,  Γ2 , .. , Γ3 }*  Ys") : C_scope.
+Hint Extern 0 (_ ##{_} _) => symmetry; eassumption.
 
 Class DisjointList A := disjoint_list : list A → Prop.
 Hint Mode DisjointList ! : typeclass_instances.
 Instance: Params (@disjoint_list) 2.
-Notation "⊥ Xs" := (disjoint_list Xs) (at level 20, format "⊥  Xs") : C_scope.
+Notation "## Xs" := (disjoint_list Xs) (at level 20, format "##  Xs") : C_scope.
 
 Section disjoint_list.
   Context `{Disjoint A, Union A, Empty A}.
   Implicit Types X : A.
 
   Inductive disjoint_list_default : DisjointList A :=
-    | disjoint_nil_2 : ⊥ (@nil A)
-    | disjoint_cons_2 (X : A) (Xs : list A) : X ⊥ ⋃ Xs → ⊥ Xs → ⊥ (X :: Xs).
+    | disjoint_nil_2 : ## (@nil A)
+    | disjoint_cons_2 (X : A) (Xs : list A) : X ## ⋃ Xs → ## Xs → ## (X :: Xs).
   Global Existing Instance disjoint_list_default.
 
-  Lemma disjoint_list_nil  : ⊥ @nil A ↔ True.
+  Lemma disjoint_list_nil  : ## @nil A ↔ True.
   Proof. split; constructor. Qed.
-  Lemma disjoint_list_cons X Xs : ⊥ (X :: Xs) ↔ X ⊥ ⋃ Xs ∧ ⊥ Xs.
+  Lemma disjoint_list_cons X Xs : ## (X :: Xs) ↔ X ## ⋃ Xs ∧ ## Xs.
   Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed.
 End disjoint_list.
 
diff --git a/theories/collections.v b/theories/collections.v
index 00522a5c..3b406830 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -186,7 +186,7 @@ Section set_unfold_simple.
   Qed.
   Global Instance set_unfold_disjoint (P Q : A → Prop) X Y :
     (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) →
-    SetUnfold (X ⊥ Y) (∀ x, P x → Q x → False).
+    SetUnfold (X ## Y) (∀ x, P x → Q x → False).
   Proof. constructor. unfold disjoint, collection_disjoint. naive_solver. Qed.
 
   Context `{!LeibnizEquiv C}.
@@ -371,9 +371,9 @@ Section simple_collection.
   Lemma empty_union X Y : X ∪ Y ≡ ∅ ↔ X ≡ ∅ ∧ Y ≡ ∅.
   Proof. set_solver. Qed.
 
-  Lemma union_cancel_l X Y Z : Z ⊥ X → Z ⊥ Y → Z ∪ X ≡ Z ∪ Y → X ≡ Y.
+  Lemma union_cancel_l X Y Z : Z ## X → Z ## Y → Z ∪ X ≡ Z ∪ Y → X ≡ Y.
   Proof. set_solver. Qed.
-  Lemma union_cancel_r X Y Z : X ⊥ Z → Y ⊥ Z → X ∪ Z ≡ Y ∪ Z → X ≡ Y.
+  Lemma union_cancel_r X Y Z : X ## Z → Y ## Z → X ∪ Z ≡ Y ∪ Z → X ≡ Y.
   Proof. set_solver. Qed.
 
   (** Empty *)
@@ -405,22 +405,22 @@ Section simple_collection.
   Proof. by rewrite elem_of_singleton. Qed.
 
   (** Disjointness *)
-  Lemma elem_of_disjoint X Y : X ⊥ Y ↔ ∀ x, x ∈ X → x ∈ Y → False.
+  Lemma elem_of_disjoint X Y : X ## Y ↔ ∀ x, x ∈ X → x ∈ Y → False.
   Proof. done. Qed.
 
   Global Instance disjoint_sym : Symmetric (@disjoint C _).
   Proof. intros X Y. set_solver. Qed.
-  Lemma disjoint_empty_l Y : ∅ ⊥ Y.
+  Lemma disjoint_empty_l Y : ∅ ## Y.
   Proof. set_solver. Qed.
-  Lemma disjoint_empty_r X : X ⊥ ∅.
+  Lemma disjoint_empty_r X : X ## ∅.
   Proof. set_solver. Qed.
-  Lemma disjoint_singleton_l x Y : {[ x ]} ⊥ Y ↔ x ∉ Y.
+  Lemma disjoint_singleton_l x Y : {[ x ]} ## Y ↔ x ∉ Y.
   Proof. set_solver. Qed.
-  Lemma disjoint_singleton_r y X : X ⊥ {[ y ]} ↔ y ∉ X.
+  Lemma disjoint_singleton_r y X : X ## {[ y ]} ↔ y ∉ X.
   Proof. set_solver. Qed.
-  Lemma disjoint_union_l X1 X2 Y : X1 ∪ X2 ⊥ Y ↔ X1 ⊥ Y ∧ X2 ⊥ Y.
+  Lemma disjoint_union_l X1 X2 Y : X1 ∪ X2 ## Y ↔ X1 ## Y ∧ X2 ## Y.
   Proof. set_solver. Qed.
-  Lemma disjoint_union_r X Y1 Y2 : X ⊥ Y1 ∪ Y2 ↔ X ⊥ Y1 ∧ X ⊥ Y2.
+  Lemma disjoint_union_r X Y1 Y2 : X ## Y1 ∪ Y2 ↔ X ## Y1 ∧ X ## Y2.
   Proof. set_solver. Qed.
 
   (** Big unions *)
@@ -494,9 +494,9 @@ Section simple_collection.
     Lemma empty_union_L X Y : X ∪ Y = ∅ ↔ X = ∅ ∧ Y = ∅.
     Proof. unfold_leibniz. apply empty_union. Qed.
 
-    Lemma union_cancel_l_L X Y Z : Z ⊥ X → Z ⊥ Y → Z ∪ X = Z ∪ Y → X = Y.
+    Lemma union_cancel_l_L X Y Z : Z ## X → Z ## Y → Z ∪ X = Z ∪ Y → X = Y.
     Proof. unfold_leibniz. apply union_cancel_l. Qed.
-    Lemma union_cancel_r_L X Y Z : X ⊥ Z → Y ⊥ Z → X ∪ Z = Y ∪ Z → X = Y.
+    Lemma union_cancel_r_L X Y Z : X ## Z → Y ## Z → X ∪ Z = Y ∪ Z → X = Y.
     Proof. unfold_leibniz. apply union_cancel_r. Qed.
 
     (** Empty *)
@@ -618,7 +618,7 @@ Section collection.
   Proof. set_solver. Qed.
   Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z.
   Proof. set_solver. Qed.
-  Lemma difference_disjoint X Y : X ⊥ Y → X ∖ Y ≡ X.
+  Lemma difference_disjoint X Y : X ## Y → X ∖ Y ≡ X.
   Proof. set_solver. Qed.
 
   Lemma difference_mono X1 X2 Y1 Y2 :
@@ -630,7 +630,7 @@ Section collection.
   Proof. set_solver. Qed.
 
   (** Disjointness *)
-  Lemma disjoint_intersection X Y : X ⊥ Y ↔ X ∩ Y ≡ ∅.
+  Lemma disjoint_intersection X Y : X ## Y ↔ X ∩ Y ≡ ∅.
   Proof. set_solver. Qed.
 
   Section leibniz.
@@ -683,11 +683,11 @@ Section collection.
     Lemma difference_intersection_distr_l_L X Y Z :
       (X ∩ Y) ∖ Z = X ∖ Z ∩ Y ∖ Z.
     Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed.
-    Lemma difference_disjoint_L X Y : X ⊥ Y → X ∖ Y = X.
+    Lemma difference_disjoint_L X Y : X ## Y → X ∖ Y = X.
     Proof. unfold_leibniz. apply difference_disjoint. Qed.
 
     (** Disjointness *)
-    Lemma disjoint_intersection_L X Y : X ⊥ Y ↔ X ∩ Y = ∅.
+    Lemma disjoint_intersection_L X Y : X ## Y ↔ X ∩ Y = ∅.
     Proof. unfold_leibniz. apply disjoint_intersection. Qed.
   End leibniz.
 
@@ -707,7 +707,7 @@ Section collection.
       intros x. rewrite !elem_of_union; rewrite elem_of_difference.
       split; [ | destruct (decide (x ∈ Y)) ]; intuition.
     Qed.
-    Lemma subseteq_disjoint_union X Y : X ⊆ Y ↔ ∃ Z, Y ≡ X ∪ Z ∧ X ⊥ Z.
+    Lemma subseteq_disjoint_union X Y : X ⊆ Y ↔ ∃ Z, Y ≡ X ∪ Z ∧ X ## Z.
     Proof.
       split; [|set_solver].
       exists (Y ∖ X); split; [auto using union_difference|set_solver].
@@ -732,7 +732,7 @@ Section collection.
     Proof. unfold_leibniz. apply non_empty_difference. Qed.
     Lemma empty_difference_subseteq_L X Y : X ∖ Y = ∅ → X ⊆ Y.
     Proof. unfold_leibniz. apply empty_difference_subseteq. Qed.
-    Lemma subseteq_disjoint_union_L X Y : X ⊆ Y ↔ ∃ Z, Y = X ∪ Z ∧ X ⊥ Z.
+    Lemma subseteq_disjoint_union_L X Y : X ⊆ Y ↔ ∃ Z, Y = X ∪ Z ∧ X ## Z.
     Proof. unfold_leibniz. apply subseteq_disjoint_union. Qed.
     Lemma singleton_union_difference_L X Y x :
       {[x]} ∪ (X ∖ Y) = ({[x]} ∪ X) ∖ (Y ∖ {[x]}).
@@ -1052,7 +1052,7 @@ Section seq_set.
   Qed.
 
   Lemma seq_set_S_disjoint start len :
-    {[ start + len ]} ⊥ seq_set (C:=C) start len.
+    {[ start + len ]} ## seq_set (C:=C) start len.
   Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed.
 
   Lemma seq_set_S_union start len :
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 15f04654..c2e6487e 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -122,7 +122,7 @@ Proof.
   - set_solver.
 Qed.
 
-Lemma size_union X Y : X ⊥ Y → size (X ∪ Y) = size X + size Y.
+Lemma size_union X Y : X ## Y → size (X ∪ Y) = size X + size Y.
 Proof.
   intros. unfold size, collection_size. simpl. rewrite <-app_length.
   apply Permutation_length, NoDup_Permutation.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 1500b623..a76c7076 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -81,14 +81,14 @@ Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed.
 Lemma delete_insert_dom {A} (m : M A) i x :
   i ∉ dom D m → delete i (<[i:=x]>m) = m.
 Proof. rewrite not_elem_of_dom. apply delete_insert. Qed.
-Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ⊥ₘ m2 ↔ dom D m1 ⊥ dom D m2.
+Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ##ₘ m2 ↔ dom D m1 ## dom D m2.
 Proof.
   rewrite map_disjoint_spec, elem_of_disjoint.
   setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.
 Qed.
-Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ⊥ₘ m2 → dom D m1 ⊥ dom D m2.
+Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ##ₘ m2 → dom D m1 ## dom D m2.
 Proof. apply map_disjoint_dom. Qed.
-Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 ⊥ dom D m2 → m1 ⊥ₘ m2.
+Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 ## dom D m2 → m1 ##ₘ m2.
 Proof. apply map_disjoint_dom. Qed.
 Lemma dom_union {A} (m1 m2 : M A) : dom D (m1 ∪ m2) ≡ dom D m1 ∪ dom D m2.
 Proof.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index b52ce660..212de812 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -92,10 +92,10 @@ Definition map_included `{∀ A, Lookup K A (M A)} {A}
   (R : relation A) : relation (M A) := map_relation R (λ _, False) (λ _, True).
 Definition map_disjoint `{∀ A, Lookup K A (M A)} {A} : relation (M A) :=
   map_relation (λ _ _, False) (λ _, True) (λ _, True).
-Infix "⊥ₘ" := map_disjoint (at level 70) : C_scope.
-Hint Extern 0 (_ ⊥ₘ _) => symmetry; eassumption.
-Notation "( m ⊥ₘ.)" := (map_disjoint m) (only parsing) : C_scope.
-Notation "(.⊥ₘ m )" := (λ m2, m2 ⊥ₘ m) (only parsing) : C_scope.
+Infix "##ₘ" := map_disjoint (at level 70) : C_scope.
+Hint Extern 0 (_ ##ₘ _) => symmetry; eassumption.
+Notation "( m ##ₘ.)" := (map_disjoint m) (only parsing) : C_scope.
+Notation "(.##ₘ m )" := (λ m2, m2 ##ₘ m) (only parsing) : C_scope.
 Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
   map_included (=).
 
@@ -1313,19 +1313,19 @@ End Forall2.
 
 (** ** Properties on the disjoint maps *)
 Lemma map_disjoint_spec {A} (m1 m2 : M A) :
-  m1 ⊥ₘ m2 ↔ ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → False.
+  m1 ##ₘ m2 ↔ ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → False.
 Proof.
   split; intros Hm i; specialize (Hm i);
     destruct (m1 !! i), (m2 !! i); naive_solver.
 Qed.
 Lemma map_disjoint_alt {A} (m1 m2 : M A) :
-  m1 ⊥ₘ m2 ↔ ∀ i, m1 !! i = None ∨ m2 !! i = None.
+  m1 ##ₘ m2 ↔ ∀ i, m1 !! i = None ∨ m2 !! i = None.
 Proof.
   split; intros Hm1m2 i; specialize (Hm1m2 i);
     destruct (m1 !! i), (m2 !! i); naive_solver.
 Qed.
 Lemma map_not_disjoint {A} (m1 m2 : M A) :
-  ¬m1 ⊥ₘ m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2.
+  ¬m1 ##ₘ m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2.
 Proof.
   unfold disjoint, map_disjoint. rewrite map_not_Forall2 by solve_decision.
   split; [|naive_solver].
@@ -1333,26 +1333,26 @@ Proof.
 Qed.
 Global Instance map_disjoint_sym : Symmetric (map_disjoint : relation (M A)).
 Proof. intros A m1 m2. rewrite !map_disjoint_spec. naive_solver. Qed.
-Lemma map_disjoint_empty_l {A} (m : M A) : ∅ ⊥ₘ m.
+Lemma map_disjoint_empty_l {A} (m : M A) : ∅ ##ₘ m.
 Proof. rewrite !map_disjoint_spec. intros i x y. by rewrite lookup_empty. Qed.
-Lemma map_disjoint_empty_r {A} (m : M A) : m ⊥ₘ ∅.
+Lemma map_disjoint_empty_r {A} (m : M A) : m ##ₘ ∅.
 Proof. rewrite !map_disjoint_spec. intros i x y. by rewrite lookup_empty. Qed.
 Lemma map_disjoint_weaken {A} (m1 m1' m2 m2' : M A) :
-  m1' ⊥ₘ m2' → m1 ⊆ m1' → m2 ⊆ m2' → m1 ⊥ₘ m2.
+  m1' ##ₘ m2' → m1 ⊆ m1' → m2 ⊆ m2' → m1 ##ₘ m2.
 Proof. rewrite !map_subseteq_spec, !map_disjoint_spec. eauto. Qed.
 Lemma map_disjoint_weaken_l {A} (m1 m1' m2  : M A) :
-  m1' ⊥ₘ m2 → m1 ⊆ m1' → m1 ⊥ₘ m2.
+  m1' ##ₘ m2 → m1 ⊆ m1' → m1 ##ₘ m2.
 Proof. eauto using map_disjoint_weaken. Qed.
 Lemma map_disjoint_weaken_r {A} (m1 m2 m2' : M A) :
-  m1 ⊥ₘ m2' → m2 ⊆ m2' → m1 ⊥ₘ m2.
+  m1 ##ₘ m2' → m2 ⊆ m2' → m1 ##ₘ m2.
 Proof. eauto using map_disjoint_weaken. Qed.
 Lemma map_disjoint_Some_l {A} (m1 m2 : M A) i x:
-  m1 ⊥ₘ m2 → m1 !! i = Some x → m2 !! i = None.
+  m1 ##ₘ m2 → m1 !! i = Some x → m2 !! i = None.
 Proof. rewrite map_disjoint_spec, eq_None_not_Some. intros ?? [??]; eauto. Qed.
 Lemma map_disjoint_Some_r {A} (m1 m2 : M A) i x:
-  m1 ⊥ₘ m2 → m2 !! i = Some x → m1 !! i = None.
+  m1 ##ₘ m2 → m2 !! i = Some x → m1 !! i = None.
 Proof. rewrite (symmetry_iff map_disjoint). apply map_disjoint_Some_l. Qed.
-Lemma map_disjoint_singleton_l {A} (m: M A) i x : {[i:=x]} ⊥ₘ m ↔ m !! i = None.
+Lemma map_disjoint_singleton_l {A} (m: M A) i x : {[i:=x]} ##ₘ m ↔ m !! i = None.
 Proof.
   split; [|rewrite !map_disjoint_spec].
   - intro. apply (map_disjoint_Some_l {[i := x]} _ _ x);
@@ -1362,20 +1362,20 @@ Proof.
     + by rewrite lookup_singleton_ne.
 Qed.
 Lemma map_disjoint_singleton_r {A} (m : M A) i x :
-  m ⊥ₘ {[i := x]} ↔ m !! i = None.
+  m ##ₘ {[i := x]} ↔ m !! i = None.
 Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_singleton_l. Qed.
 Lemma map_disjoint_singleton_l_2 {A} (m : M A) i x :
-  m !! i = None → {[i := x]} ⊥ₘ m.
+  m !! i = None → {[i := x]} ##ₘ m.
 Proof. by rewrite map_disjoint_singleton_l. Qed.
 Lemma map_disjoint_singleton_r_2 {A} (m : M A) i x :
-  m !! i = None → m ⊥ₘ {[i := x]}.
+  m !! i = None → m ##ₘ {[i := x]}.
 Proof. by rewrite map_disjoint_singleton_r. Qed.
-Lemma map_disjoint_delete_l {A} (m1 m2 : M A) i : m1 ⊥ₘ m2 → delete i m1 ⊥ₘ m2.
+Lemma map_disjoint_delete_l {A} (m1 m2 : M A) i : m1 ##ₘ m2 → delete i m1 ##ₘ m2.
 Proof.
   rewrite !map_disjoint_alt. intros Hdisjoint j. destruct (Hdisjoint j); auto.
   rewrite lookup_delete_None. tauto.
 Qed.
-Lemma map_disjoint_delete_r {A} (m1 m2 : M A) i : m1 ⊥ₘ m2 → m1 ⊥ₘ delete i m2.
+Lemma map_disjoint_delete_r {A} (m1 m2 : M A) i : m1 ##ₘ m2 → m1 ##ₘ delete i m2.
 Proof. symmetry. by apply map_disjoint_delete_l. Qed.
 
 (** ** Properties of the [union_with] operation *)
@@ -1495,7 +1495,7 @@ Qed.
 Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 ≠ ∅ → m1 ∪ m2 ≠ ∅.
 Proof. eauto using map_positive_l. Qed.
 Lemma lookup_union_Some {A} (m1 m2 : M A) i x :
-  m1 ⊥ₘ m2 → (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ m2 !! i = Some x.
+  m1 ##ₘ m2 → (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ m2 !! i = Some x.
 Proof.
   intros Hdisjoint. rewrite lookup_union_Some_raw.
   intuition eauto using map_disjoint_Some_r.
@@ -1504,9 +1504,9 @@ Lemma lookup_union_Some_l {A} (m1 m2 : M A) i x :
   m1 !! i = Some x → (m1 ∪ m2) !! i = Some x.
 Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed.
 Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x :
-  m1 ⊥ₘ m2 → m2 !! i = Some x → (m1 ∪ m2) !! i = Some x.
+  m1 ##ₘ m2 → m2 !! i = Some x → (m1 ∪ m2) !! i = Some x.
 Proof. intro. rewrite lookup_union_Some; intuition. Qed.
-Lemma map_union_comm {A} (m1 m2 : M A) : m1 ⊥ₘ m2 → m1 ∪ m2 = m2 ∪ m1.
+Lemma map_union_comm {A} (m1 m2 : M A) : m1 ##ₘ m2 → m1 ∪ m2 = m2 ∪ m1.
 Proof.
   intros Hdisjoint. apply (merge_comm (union_with (λ x _, Some x))).
   intros i. specialize (Hdisjoint i).
@@ -1524,14 +1524,14 @@ Lemma map_union_subseteq_l {A} (m1 m2 : M A) : m1 ⊆ m1 ∪ m2.
 Proof.
   rewrite map_subseteq_spec. intros ? i x. rewrite lookup_union_Some_raw. tauto.
 Qed.
-Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1 ⊥ₘ m2 → m2 ⊆ m1 ∪ m2.
+Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1 ##ₘ m2 → m2 ⊆ m1 ∪ m2.
 Proof.
   intros. rewrite map_union_comm by done. by apply map_union_subseteq_l.
 Qed.
 Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m1 ⊆ m2 ∪ m3.
 Proof. intros. trans m2; auto using map_union_subseteq_l. Qed.
 Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) :
-  m2 ⊥ₘ m3 → m1 ⊆ m3 → m1 ⊆ m2 ∪ m3.
+  m2 ##ₘ m3 → m1 ⊆ m3 → m1 ⊆ m2 ∪ m3.
 Proof. intros. trans m3; auto using map_union_subseteq_r. Qed.
 Lemma map_union_mono_l {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m3 ∪ m1 ⊆ m3 ∪ m2.
 Proof.
@@ -1539,52 +1539,52 @@ Proof.
   rewrite !lookup_union_Some_raw. naive_solver.
 Qed.
 Lemma map_union_mono_r {A} (m1 m2 m3 : M A) :
-  m2 ⊥ₘ m3 → m1 ⊆ m2 → m1 ∪ m3 ⊆ m2 ∪ m3.
+  m2 ##ₘ m3 → m1 ⊆ m2 → m1 ∪ m3 ⊆ m2 ∪ m3.
 Proof.
   intros. rewrite !(map_union_comm _ m3)
     by eauto using map_disjoint_weaken_l.
   by apply map_union_mono_l.
 Qed.
 Lemma map_union_reflecting_l {A} (m1 m2 m3 : M A) :
-  m3 ⊥ₘ m1 → m3 ⊥ₘ m2 → m3 ∪ m1 ⊆ m3 ∪ m2 → m1 ⊆ m2.
+  m3 ##ₘ m1 → m3 ##ₘ m2 → m3 ∪ m1 ⊆ m3 ∪ m2 → m1 ⊆ m2.
 Proof.
   rewrite !map_subseteq_spec. intros Hm31 Hm32 Hm i x ?. specialize (Hm i x).
   rewrite !lookup_union_Some in Hm by done. destruct Hm; auto.
   by rewrite map_disjoint_spec in Hm31; destruct (Hm31 i x x).
 Qed.
 Lemma map_union_reflecting_r {A} (m1 m2 m3 : M A) :
-  m1 ⊥ₘ m3 → m2 ⊥ₘ m3 → m1 ∪ m3 ⊆ m2 ∪ m3 → m1 ⊆ m2.
+  m1 ##ₘ m3 → m2 ##ₘ m3 → m1 ∪ m3 ⊆ m2 ∪ m3 → m1 ⊆ m2.
 Proof.
   intros ??. rewrite !(map_union_comm _ m3) by done.
   by apply map_union_reflecting_l.
 Qed.
 Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) :
-  m1 ⊥ₘ m3 → m2 ⊥ₘ m3 → m3 ∪ m1 = m3 ∪ m2 → m1 = m2.
+  m1 ##ₘ m3 → m2 ##ₘ m3 → m3 ∪ m1 = m3 ∪ m2 → m1 = m2.
 Proof.
   intros. apply (anti_symm (⊆)); apply map_union_reflecting_l with m3;
     auto using (reflexive_eq (R:=@subseteq (M A) _)).
 Qed.
 Lemma map_union_cancel_r {A} (m1 m2 m3 : M A) :
-  m1 ⊥ₘ m3 → m2 ⊥ₘ m3 → m1 ∪ m3 = m2 ∪ m3 → m1 = m2.
+  m1 ##ₘ m3 → m2 ##ₘ m3 → m1 ∪ m3 = m2 ∪ m3 → m1 = m2.
 Proof.
   intros. apply (anti_symm (⊆)); apply map_union_reflecting_r with m3;
     auto using (reflexive_eq (R:=@subseteq (M A) _)).
 Qed.
 Lemma map_disjoint_union_l {A} (m1 m2 m3 : M A) :
-  m1 ∪ m2 ⊥ₘ m3 ↔ m1 ⊥ₘ m3 ∧ m2 ⊥ₘ m3.
+  m1 ∪ m2 ##ₘ m3 ↔ m1 ##ₘ m3 ∧ m2 ##ₘ m3.
 Proof.
   rewrite !map_disjoint_alt. setoid_rewrite lookup_union_None. naive_solver.
 Qed.
 Lemma map_disjoint_union_r {A} (m1 m2 m3 : M A) :
-  m1 ⊥ₘ m2 ∪ m3 ↔ m1 ⊥ₘ m2 ∧ m1 ⊥ₘ m3.
+  m1 ##ₘ m2 ∪ m3 ↔ m1 ##ₘ m2 ∧ m1 ##ₘ m3.
 Proof.
   rewrite !map_disjoint_alt. setoid_rewrite lookup_union_None. naive_solver.
 Qed.
 Lemma map_disjoint_union_l_2 {A} (m1 m2 m3 : M A) :
-  m1 ⊥ₘ m3 → m2 ⊥ₘ m3 → m1 ∪ m2 ⊥ₘ m3.
+  m1 ##ₘ m3 → m2 ##ₘ m3 → m1 ∪ m2 ##ₘ m3.
 Proof. by rewrite map_disjoint_union_l. Qed.
 Lemma map_disjoint_union_r_2 {A} (m1 m2 m3 : M A) :
-  m1 ⊥ₘ m2 → m1 ⊥ₘ m3 → m1 ⊥ₘ m2 ∪ m3.
+  m1 ##ₘ m2 → m1 ##ₘ m3 → m1 ##ₘ m2 ∪ m3.
 Proof. by rewrite map_disjoint_union_r. Qed.
 Lemma insert_union_singleton_l {A} (m : M A) i x : <[i:=x]>m = {[i := x]} ∪ m.
 Proof.
@@ -1601,22 +1601,22 @@ Proof.
   by apply map_disjoint_singleton_l.
 Qed.
 Lemma map_disjoint_insert_l {A} (m1 m2 : M A) i x :
-  <[i:=x]>m1 ⊥ₘ m2 ↔ m2 !! i = None ∧ m1 ⊥ₘ m2.
+  <[i:=x]>m1 ##ₘ m2 ↔ m2 !! i = None ∧ m1 ##ₘ m2.
 Proof.
   rewrite insert_union_singleton_l.
   by rewrite map_disjoint_union_l, map_disjoint_singleton_l.
 Qed.
 Lemma map_disjoint_insert_r {A} (m1 m2 : M A) i x :
-  m1 ⊥ₘ <[i:=x]>m2 ↔ m1 !! i = None ∧ m1 ⊥ₘ m2.
+  m1 ##ₘ <[i:=x]>m2 ↔ m1 !! i = None ∧ m1 ##ₘ m2.
 Proof.
   rewrite insert_union_singleton_l.
   by rewrite map_disjoint_union_r, map_disjoint_singleton_r.
 Qed.
 Lemma map_disjoint_insert_l_2 {A} (m1 m2 : M A) i x :
-  m2 !! i = None → m1 ⊥ₘ m2 → <[i:=x]>m1 ⊥ₘ m2.
+  m2 !! i = None → m1 ##ₘ m2 → <[i:=x]>m1 ##ₘ m2.
 Proof. by rewrite map_disjoint_insert_l. Qed.
 Lemma map_disjoint_insert_r_2 {A} (m1 m2 : M A) i x :
-  m1 !! i = None → m1 ⊥ₘ m2 → m1 ⊥ₘ <[i:=x]>m2.
+  m1 !! i = None → m1 ##ₘ m2 → m1 ##ₘ <[i:=x]>m2.
 Proof. by rewrite map_disjoint_insert_r. Qed.
 Lemma insert_union_l {A} (m1 m2 : M A) i x :
   <[i:=x]>(m1 ∪ m2) = <[i:=x]>m1 ∪ m2.
@@ -1640,7 +1640,7 @@ Proof. apply delete_union_with. Qed.
 
 (** ** Properties of the [union_list] operation *)
 Lemma map_disjoint_union_list_l {A} (ms : list (M A)) (m : M A) :
-  ⋃ ms ⊥ₘ m ↔ Forall (.⊥ₘ m) ms.
+  ⋃ ms ##ₘ m ↔ Forall (.##ₘ m) ms.
 Proof.
   split.
   - induction ms; simpl; rewrite ?map_disjoint_union_l; intuition.
@@ -1648,13 +1648,13 @@ Proof.
     by rewrite map_disjoint_union_l.
 Qed.
 Lemma map_disjoint_union_list_r {A} (ms : list (M A)) (m : M A) :
-  m ⊥ₘ ⋃ ms ↔ Forall (.⊥ₘ m) ms.
+  m ##ₘ ⋃ ms ↔ Forall (.##ₘ m) ms.
 Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_union_list_l. Qed.
 Lemma map_disjoint_union_list_l_2 {A} (ms : list (M A)) (m : M A) :
-  Forall (.⊥ₘ m) ms → ⋃ ms ⊥ₘ m.
+  Forall (.##ₘ m) ms → ⋃ ms ##ₘ m.
 Proof. by rewrite map_disjoint_union_list_l. Qed.
 Lemma map_disjoint_union_list_r_2 {A} (ms : list (M A)) (m : M A) :
-  Forall (.⊥ₘ m) ms → m ⊥ₘ ⋃ ms.
+  Forall (.##ₘ m) ms → m ##ₘ ⋃ ms.
 Proof. by rewrite map_disjoint_union_list_r. Qed.
 
 (** ** Properties of the folding the [delete] function *)
@@ -1681,10 +1681,10 @@ Proof.
   rewrite IHis, delete_insert_ne; intuition.
 Qed.
 Lemma map_disjoint_foldr_delete_l {A} (m1 m2 : M A) is :
-  m1 ⊥ₘ m2 → foldr delete m1 is ⊥ₘ m2.
+  m1 ##ₘ m2 → foldr delete m1 is ##ₘ m2.
 Proof. induction is; simpl; auto using map_disjoint_delete_l. Qed.
 Lemma map_disjoint_foldr_delete_r {A} (m1 m2 : M A) is :
-  m1 ⊥ₘ m2 → m1 ⊥ₘ foldr delete m2 is.
+  m1 ##ₘ m2 → m1 ##ₘ foldr delete m2 is.
 Proof. induction is; simpl; auto using map_disjoint_delete_r. Qed.
 Lemma foldr_delete_union {A} (m1 m2 : M A) is :
   foldr delete (m1 ∪ m2) is = foldr delete m1 is ∪ foldr delete m2 is.
@@ -1692,7 +1692,7 @@ Proof. apply foldr_delete_union_with. Qed.
 
 (** ** Properties on disjointness of conversion to lists *)
 Lemma map_disjoint_of_list_l {A} (m : M A) ixs :
-  map_of_list ixs ⊥ₘ m ↔ Forall (λ ix, m !! ix.1 = None) ixs.
+  map_of_list ixs ##ₘ m ↔ Forall (λ ix, m !! ix.1 = None) ixs.
 Proof.
   split.
   - induction ixs; simpl; rewrite ?map_disjoint_insert_l in *; intuition.
@@ -1700,28 +1700,28 @@ Proof.
     rewrite map_disjoint_insert_l. auto.
 Qed.
 Lemma map_disjoint_of_list_r {A} (m : M A) ixs :
-  m ⊥ₘ map_of_list ixs ↔ Forall (λ ix, m !! ix.1 = None) ixs.
+  m ##ₘ map_of_list ixs ↔ Forall (λ ix, m !! ix.1 = None) ixs.
 Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_of_list_l. Qed.
 Lemma map_disjoint_of_list_zip_l {A} (m : M A) is xs :
   length is = length xs →
-  map_of_list (zip is xs) ⊥ₘ m ↔ Forall (λ i, m !! i = None) is.
+  map_of_list (zip is xs) ##ₘ m ↔ Forall (λ i, m !! i = None) is.
 Proof.
   intro. rewrite map_disjoint_of_list_l.
   rewrite <-(fst_zip is xs) at 2 by lia. by rewrite Forall_fmap.
 Qed.
 Lemma map_disjoint_of_list_zip_r {A} (m : M A) is xs :
   length is = length xs →
-  m ⊥ₘ map_of_list (zip is xs) ↔ Forall (λ i, m !! i = None) is.
+  m ##ₘ map_of_list (zip is xs) ↔ Forall (λ i, m !! i = None) is.
 Proof.
   intro. by rewrite (symmetry_iff map_disjoint), map_disjoint_of_list_zip_l.
 Qed.
 Lemma map_disjoint_of_list_zip_l_2 {A} (m : M A) is xs :
   length is = length xs → Forall (λ i, m !! i = None) is →
-  map_of_list (zip is xs) ⊥ₘ m.
+  map_of_list (zip is xs) ##ₘ m.
 Proof. intro. by rewrite map_disjoint_of_list_zip_l. Qed.
 Lemma map_disjoint_of_list_zip_r_2 {A} (m : M A) is xs :
   length is = length xs → Forall (λ i, m !! i = None) is →
-  m ⊥ₘ map_of_list (zip is xs).
+  m ##ₘ map_of_list (zip is xs).
 Proof. intro. by rewrite map_disjoint_of_list_zip_r. Qed.
 
 (** ** Properties of the [intersection_with] operation *)
@@ -1776,13 +1776,13 @@ Proof.
   unfold difference, map_difference; rewrite lookup_difference_with.
   destruct (m1 !! i), (m2 !! i); compute; naive_solver.
 Qed.
-Lemma map_disjoint_difference_l {A} (m1 m2 : M A) : m1 ⊆ m2 → m2 ∖ m1 ⊥ₘ m1.
+Lemma map_disjoint_difference_l {A} (m1 m2 : M A) : m1 ⊆ m2 → m2 ∖ m1 ##ₘ m1.
 Proof.
   intros Hm i; specialize (Hm i).
   unfold difference, map_difference; rewrite lookup_difference_with.
   by destruct (m1 !! i), (m2 !! i).
 Qed.
-Lemma map_disjoint_difference_r {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ⊥ₘ m2 ∖ m1.
+Lemma map_disjoint_difference_r {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ##ₘ m2 ∖ m1.
 Proof. intros. symmetry. by apply map_disjoint_difference_l. Qed.
 Lemma map_difference_union {A} (m1 m2 : M A) :
   m1 ⊆ m2 → m1 ∪ m2 ∖ m1 = m2.
@@ -1804,20 +1804,20 @@ maps. This tactic does not yield any information loss as all simplifications
 performed are reversible. *)
 Ltac decompose_map_disjoint := repeat
   match goal with
-  | H : _ ∪ _ ⊥ₘ _ |- _ => apply map_disjoint_union_l in H; destruct H
-  | H : _ ⊥ₘ _ ∪ _ |- _ => apply map_disjoint_union_r in H; destruct H
-  | H : {[ _ := _ ]} ⊥ₘ _ |- _ => apply map_disjoint_singleton_l in H
-  | H : _ ⊥ₘ {[ _ := _ ]} |- _ =>  apply map_disjoint_singleton_r in H
-  | H : <[_:=_]>_ ⊥ₘ _ |- _ => apply map_disjoint_insert_l in H; destruct H
-  | H : _ ⊥ₘ <[_:=_]>_ |- _ => apply map_disjoint_insert_r in H; destruct H
-  | H : ⋃ _ ⊥ₘ _ |- _ => apply map_disjoint_union_list_l in H
-  | H : _ ⊥ₘ ⋃ _ |- _ => apply map_disjoint_union_list_r in H
-  | H : ∅ ⊥ₘ _ |- _ => clear H
-  | H : _ ⊥ₘ ∅ |- _ => clear H
-  | H : Forall (.⊥ₘ _) _ |- _ => rewrite Forall_vlookup in H
-  | H : Forall (.⊥ₘ _) [] |- _ => clear H
-  | H : Forall (.⊥ₘ _) (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
-  | H : Forall (.⊥ₘ _) (_ :: _) |- _ => rewrite Forall_app in H; destruct H
+  | H : _ ∪ _ ##ₘ _ |- _ => apply map_disjoint_union_l in H; destruct H
+  | H : _ ##ₘ _ ∪ _ |- _ => apply map_disjoint_union_r in H; destruct H
+  | H : {[ _ := _ ]} ##ₘ _ |- _ => apply map_disjoint_singleton_l in H
+  | H : _ ##ₘ {[ _ := _ ]} |- _ =>  apply map_disjoint_singleton_r in H
+  | H : <[_:=_]>_ ##ₘ _ |- _ => apply map_disjoint_insert_l in H; destruct H
+  | H : _ ##ₘ <[_:=_]>_ |- _ => apply map_disjoint_insert_r in H; destruct H
+  | H : ⋃ _ ##ₘ _ |- _ => apply map_disjoint_union_list_l in H
+  | H : _ ##ₘ ⋃ _ |- _ => apply map_disjoint_union_list_r in H
+  | H : ∅ ##ₘ _ |- _ => clear H
+  | H : _ ##ₘ ∅ |- _ => clear H
+  | H : Forall (.##ₘ _) _ |- _ => rewrite Forall_vlookup in H
+  | H : Forall (.##ₘ _) [] |- _ => clear H
+  | H : Forall (.##ₘ _) (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
+  | H : Forall (.##ₘ _) (_ :: _) |- _ => rewrite Forall_app in H; destruct H
   end.
 
 (** To prove a disjointness property, we first decompose all hypotheses, and
@@ -1828,28 +1828,28 @@ Ltac solve_map_disjoint :=
 
 (** We declare these hints using [Hint Extern] instead of [Hint Resolve] as
 [eauto] works badly with hints parametrized by type class constraints. *)
-Hint Extern 1 (_ ⊥ₘ _) => done : map_disjoint.
-Hint Extern 2 (∅ ⊥ₘ _) => apply map_disjoint_empty_l : map_disjoint.
-Hint Extern 2 (_ ⊥ₘ ∅) => apply map_disjoint_empty_r : map_disjoint.
-Hint Extern 2 ({[ _ := _ ]} ⊥ₘ _) =>
+Hint Extern 1 (_ ##ₘ _) => done : map_disjoint.
+Hint Extern 2 (∅ ##ₘ _) => apply map_disjoint_empty_l : map_disjoint.
+Hint Extern 2 (_ ##ₘ ∅) => apply map_disjoint_empty_r : map_disjoint.
+Hint Extern 2 ({[ _ := _ ]} ##ₘ _) =>
   apply map_disjoint_singleton_l_2 : map_disjoint.
-Hint Extern 2 (_ ⊥ₘ {[ _ := _ ]}) =>
+Hint Extern 2 (_ ##ₘ {[ _ := _ ]}) =>
   apply map_disjoint_singleton_r_2 : map_disjoint.
-Hint Extern 2 (_ ∪ _ ⊥ₘ _) => apply map_disjoint_union_l_2 : map_disjoint.
-Hint Extern 2 (_ ⊥ₘ _ ∪ _) => apply map_disjoint_union_r_2 : map_disjoint.
-Hint Extern 2 (<[_:=_]>_ ⊥ₘ _) => apply map_disjoint_insert_l_2 : map_disjoint.
-Hint Extern 2 (_ ⊥ₘ <[_:=_]>_) => apply map_disjoint_insert_r_2 : map_disjoint.
-Hint Extern 2 (delete _ _ ⊥ₘ _) => apply map_disjoint_delete_l : map_disjoint.
-Hint Extern 2 (_ ⊥ₘ delete _ _) => apply map_disjoint_delete_r : map_disjoint.
-Hint Extern 2 (map_of_list _ ⊥ₘ _) =>
+Hint Extern 2 (_ ∪ _ ##ₘ _) => apply map_disjoint_union_l_2 : map_disjoint.
+Hint Extern 2 (_ ##ₘ _ ∪ _) => apply map_disjoint_union_r_2 : map_disjoint.
+Hint Extern 2 (<[_:=_]>_ ##ₘ _) => apply map_disjoint_insert_l_2 : map_disjoint.
+Hint Extern 2 (_ ##ₘ <[_:=_]>_) => apply map_disjoint_insert_r_2 : map_disjoint.
+Hint Extern 2 (delete _ _ ##ₘ _) => apply map_disjoint_delete_l : map_disjoint.
+Hint Extern 2 (_ ##ₘ delete _ _) => apply map_disjoint_delete_r : map_disjoint.
+Hint Extern 2 (map_of_list _ ##ₘ _) =>
   apply map_disjoint_of_list_zip_l_2 : mem_disjoint.
-Hint Extern 2 (_ ⊥ₘ map_of_list _) =>
+Hint Extern 2 (_ ##ₘ map_of_list _) =>
   apply map_disjoint_of_list_zip_r_2 : mem_disjoint.
-Hint Extern 2 (⋃ _ ⊥ₘ _) => apply map_disjoint_union_list_l_2 : mem_disjoint.
-Hint Extern 2 (_ ⊥ₘ ⋃ _) => apply map_disjoint_union_list_r_2 : mem_disjoint.
-Hint Extern 2 (foldr delete _ _ ⊥ₘ _) =>
+Hint Extern 2 (⋃ _ ##ₘ _) => apply map_disjoint_union_list_l_2 : mem_disjoint.
+Hint Extern 2 (_ ##ₘ ⋃ _) => apply map_disjoint_union_list_r_2 : mem_disjoint.
+Hint Extern 2 (foldr delete _ _ ##ₘ _) =>
   apply map_disjoint_foldr_delete_l : map_disjoint.
-Hint Extern 2 (_ ⊥ₘ foldr delete _ _) =>
+Hint Extern 2 (_ ##ₘ foldr delete _ _) =>
   apply map_disjoint_foldr_delete_r : map_disjoint.
 
 (** The tactic [simpl_map by tac] simplifies occurrences of finite map look
-- 
GitLab