diff --git a/theories/base.v b/theories/base.v
index 4823508f0879b34a5a99d2c31509b4b2cd0497ab..adc16d87b36967dfc3c2bddbd03799e13490eb58 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -23,6 +23,7 @@ Arguments compose _ _ _ _ _ _ /.
 Arguments flip _ _ _ _ _ _ /.
 Arguments const _ _ _ _ /.
 Typeclasses Transparent id compose flip const.
+Instance: Params (@pair) 2.
 
 (** Change [True] and [False] into notations in order to enable overloading.
 We will use this in the file [assertions] to give [True] and [False] a
@@ -792,6 +793,11 @@ Instance pointwise_transitive {A} `{R : relation B} :
   Transitive R → Transitive (pointwise_relation A R) | 9.
 Proof. firstorder. Qed.
 
+(** ** Unit *)
+Instance unit_equiv : Equiv unit := λ _ _, True.
+Instance unit_equivalence : Equivalence (@equiv unit _).
+Proof. repeat split. Qed.
+
 (** ** Products *)
 Instance prod_map_injective {A A' B B'} (f : A → A') (g : B → B') :
   Injective (=) (=) f → Injective (=) (=) g →
@@ -825,6 +831,15 @@ Section prod_relation.
   Proof. firstorder eauto. Qed.
 End prod_relation.
 
+Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation (≡) (≡).
+Instance pair_proper `{Equiv A, Equiv B} :
+  Proper ((≡) ==> (≡) ==> (≡)) (@pair A B) | 0 := _.
+Instance fst_proper `{Equiv A, Equiv B} :
+  Proper ((≡) ==> (≡)) (@fst A B) | 0 := _.
+Instance snd_proper `{Equiv A, Equiv B} :
+  Proper ((≡) ==> (≡)) (@snd A B) | 0 := _.
+Typeclasses Opaque prod_equiv.
+
 (** ** Other *)
 Lemma or_l P Q : ¬Q → P ∨ Q ↔ P.
 Proof. tauto. Qed.
diff --git a/theories/collections.v b/theories/collections.v
index 281f7ef3448a0b1c4ed528137719fbdb9c30a489..eaff59e01b0132b99b2a8bf59f6a423aecabfece 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -249,7 +249,7 @@ Ltac unfold_elem_of :=
 For goals that do not involve [≡], [⊆], [map], or quantifiers this tactic is
 generally powerful enough. This tactic either fails or proves the goal. *)
 Tactic Notation "solve_elem_of" tactic3(tac) :=
-  simpl in *;
+  setoid_subst;
   decompose_empty;
   unfold_elem_of;
   solve [intuition (simplify_equality; tac)].
@@ -261,7 +261,7 @@ fails or loops on very small goals generated by [solve_elem_of] already. We
 use the [naive_solver] tactic as a substitute. This tactic either fails or
 proves the goal. *)
 Tactic Notation "esolve_elem_of" tactic3(tac) :=
-  simpl in *;
+  setoid_subst;
   decompose_empty;
   unfold_elem_of;
   naive_solver tac.
@@ -273,6 +273,11 @@ Section collection.
 
   Global Instance: Lattice C.
   Proof. split. apply _. firstorder auto. solve_elem_of. Qed.
+  Global Instance difference_proper : Proper ((≡) ==> (≡) ==> (≡)) (∖).
+  Proof.
+    intros X1 X2 HX Y1 Y2 HY; apply elem_of_equiv; intros x.
+    by rewrite !elem_of_difference, HX, HY.
+  Qed.
   Lemma intersection_singletons x : {[x]} ∩ {[x]} ≡ {[x]}.
   Proof. esolve_elem_of. Qed.
   Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y.
@@ -283,6 +288,8 @@ Section collection.
   Proof. esolve_elem_of. Qed.
   Lemma difference_union_distr_l X Y Z : (X ∪ Y) ∖ Z ≡ X ∖ Z ∪ Y ∖ Z.
   Proof. esolve_elem_of. Qed.
+  Lemma difference_union_distr_r X Y Z : Z ∖ (X ∪ Y) ≡ (Z ∖ X) ∩ (Z ∖ Y).
+  Proof. esolve_elem_of. Qed.
   Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z.
   Proof. esolve_elem_of. Qed.
 
@@ -298,6 +305,8 @@ Section collection.
     Proof. unfold_leibniz. apply difference_diag. Qed.
     Lemma difference_union_distr_l_L X Y Z : (X ∪ Y) ∖ Z = X ∖ Z ∪ Y ∖ Z.
     Proof. unfold_leibniz. apply difference_union_distr_l. Qed.
+    Lemma difference_union_distr_r_L X Y Z : Z ∖ (X ∪ Y) = (Z ∖ X) ∩ (Z ∖ Y).
+    Proof. unfold_leibniz. apply difference_union_distr_r. Qed.
     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.
@@ -518,16 +527,13 @@ Section collection_monad.
 
   Global Instance collection_fmap_proper {A B} (f : A → B) :
     Proper ((≡) ==> (≡)) (fmap f).
-  Proof. intros X Y E. esolve_elem_of. Qed.
-  Global Instance collection_ret_proper {A} :
-    Proper ((=) ==> (≡)) (@mret M _ A).
-  Proof. intros X Y E. esolve_elem_of. Qed.
+  Proof. intros X Y [??]; split; esolve_elem_of. Qed.
   Global Instance collection_bind_proper {A B} (f : A → M B) :
     Proper ((≡) ==> (≡)) (mbind f).
-  Proof. intros X Y E. esolve_elem_of. Qed.
+  Proof. intros X Y [??]; split; esolve_elem_of. Qed.
   Global Instance collection_join_proper {A} :
     Proper ((≡) ==> (≡)) (@mjoin M _ A).
-  Proof. intros X Y E. esolve_elem_of. Qed.
+  Proof. intros X Y [??]; split; esolve_elem_of. Qed.
 
   Lemma collection_bind_singleton {A B} (f : A → M B) x : {[ x ]} ≫= f ≡ f x.
   Proof. esolve_elem_of. Qed.
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 0b3789bafd479a4f6be898ae08b35cb84d452b99..f4e63f636e3e26fa67d75ea4b60305d15703dc2e 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -3,7 +3,7 @@
 (** This file collects definitions and theorems on finite collections. Most
 importantly, it implements a fold and size function and some useful induction
 principles on finite collections . *)
-Require Import Permutation ars listset.
+Require Import Permutation relations listset.
 Require Export numbers collections.
 
 Instance collection_size `{Elements A C} : Size C := length ∘ elements.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 6a86cb41d0a404af509a8a41a0232cdb0f9cc690..bbdbb8ea6077d104071e28c8d379cf3d8cc66fab 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -77,15 +77,15 @@ 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_equiv_empty.
   setoid_rewrite elem_of_intersection.
   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 5a3b8df1ddd52e64268999b73c20328e247cac4c..a8a46783b024c78041b85dea55d7701dbe979f4d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -5,7 +5,7 @@ finite maps and collects some theory on it. Most importantly, it proves useful
 induction principles for finite maps and implements the tactic
 [simplify_map_equality] to simplify goals involving finite maps. *)
 Require Import Permutation.
-Require Export ars vector orders.
+Require Export relations vector orders.
 
 (** * Axiomatization of finite maps *)
 (** We require Leibniz equality to be extensional on finite maps. This of
@@ -71,25 +71,26 @@ Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
 Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) :=
   λ f, merge (difference_with f).
 
+Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 1 := λ m1 m2,
+  ∀ i, m1 !! i ≡ m2 !! i.
+
 (** The relation [intersection_forall R] on finite maps describes that the
 relation [R] holds for each pair in the intersection. *)
 Definition map_Forall `{Lookup K A M} (P : K → A → Prop) : M → Prop :=
   λ m, ∀ i x, m !! i = Some x → P i x.
-Definition map_Forall2 `{∀ A, Lookup K A (M A)} {A B}
-    (R : A → B → Prop) (P : A → Prop) (Q : B → Prop)
-    (m1 : M A) (m2 : M B) : Prop := ∀ i,
-  match m1 !! i, m2 !! i with
-  | Some x, Some y => R x y
-  | Some x, None => P x
-  | None, Some y => Q y
-  | None, None => True
-  end.
+Definition map_relation `{∀ A, Lookup K A (M A)} {A B} (R : A → B → Prop)
+    (P : A → Prop) (Q : B → Prop) (m1 : M A) (m2 : M B) : Prop := ∀ i,
+  option_relation R P Q (m1 !! i) (m2 !! i).
 Definition map_included `{∀ A, Lookup K A (M A)} {A}
-  (R : relation A) : relation (M A) := map_Forall2 R (λ _, False) (λ _, True).
-Instance map_disjoint `{∀ A, Lookup K A (M A)} {A} : Disjoint (M A) :=
-  map_Forall2 (λ _ _, False) (λ _, True) (λ _, True).
+  (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.
 Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
-  map_Forall2 (=) (λ _, False) (λ _, True).
+  map_included (=).
 
 (** The union of two finite maps only has a meaningful definition for maps
 that are disjoint. However, as working with partial functions is inconvenient
@@ -114,12 +115,67 @@ Definition map_imap `{∀ A, Insert K A (M A), ∀ A, Empty (M A),
 Section theorems.
 Context `{FinMap K M}.
 
+(** ** Setoids *)
+Section setoid.
+  Context `{Equiv A}.
+  Global Instance map_equivalence `{!Equivalence ((≡) : relation A)} :
+    Equivalence ((≡) : relation (M A)).
+  Proof.
+    split.
+    * by intros m i.
+    * by intros m1 m2 ? i.
+    * by intros m1 m2 m3 ?? i; transitivity (m2 !! i).
+  Qed.
+  Global Instance lookup_proper (i : K) :
+    Proper ((≡) ==> (≡)) (lookup (M:=M A) i).
+  Proof. by intros m1 m2 Hm. Qed.
+  Global Instance partial_alter_proper :
+    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) partial_alter.
+  Proof.
+    by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|];
+      rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne by done;
+      try apply Hf; apply lookup_proper.
+  Qed.
+  Global Instance insert_proper (i : K) :
+    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=M A) i).
+  Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
+  Global Instance delete_proper (i : K) :
+    Proper ((≡) ==> (≡)) (delete (M:=M A) i).
+  Proof. by apply partial_alter_proper; [constructor|]. Qed.
+  Global Instance alter_proper :
+    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (alter (A:=A) (M:=M A)).
+  Proof.
+    intros ?? Hf; apply partial_alter_proper.
+    by destruct 1; constructor; apply Hf.
+  Qed.
+  Lemma merge_ext f g
+      `{!PropHolds (f None None = None), !PropHolds (g None None = None)} :
+    ((≡) ==> (≡) ==> (≡))%signature f g →
+    ((≡) ==> (≡) ==> (≡))%signature (merge f) (merge g).
+  Proof.
+    by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge by done; apply Hf.
+  Qed.
+  Global Instance union_with_proper :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==> (≡)) union_with.
+  Proof.
+    intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
+    by do 2 destruct 1; first [apply Hf | constructor].
+  Qed.    
+  Global Instance map_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (M A).
+  Proof.
+    intros m1 m2; split.
+    * by intros Hm; apply map_eq; intros i; unfold_leibniz; apply lookup_proper.
+    * by intros <-; intros i; fold_leibniz.
+  Qed.
+End setoid.
+
+(** ** General properties *)
 Lemma map_eq_iff {A} (m1 m2 : M A) : m1 = m2 ↔ ∀ i, m1 !! i = m2 !! i.
 Proof. split. by intros ->. apply map_eq. Qed.
 Lemma map_subseteq_spec {A} (m1 m2 : M A) :
   m1 ⊆ m2 ↔ ∀ i x, m1 !! i = Some x → m2 !! i = Some x.
 Proof.
-  unfold subseteq, map_subseteq, map_Forall2. split; intros Hm i;
+  unfold subseteq, map_subseteq, map_relation. split; intros Hm i;
     specialize (Hm i); destruct (m1 !! i), (m2 !! i); naive_solver.
 Qed.
 Global Instance: EmptySpec (M A).
@@ -129,9 +185,10 @@ Proof.
 Qed.
 Global Instance: ∀ {A} (R : relation A), PreOrder R → PreOrder (map_included R).
 Proof.
-  split; [intros m i; by destruct (m !! i)|].
+  split; [intros m i; by destruct (m !! i); simpl|].
   intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i).
-  destruct (m1 !! i), (m2 !! i), (m3 !! i); try done; etransitivity; eauto.
+  destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_equality';
+    done || etransitivity; eauto.
 Qed.
 Global Instance: PartialOrder ((⊆) : relation (M A)).
 Proof.
@@ -357,8 +414,8 @@ Lemma insert_included {A} R `{!Reflexive R} (m : M A) i x :
   (∀ y, m !! i = Some y → R y x) → map_included R m (<[i:=x]>m).
 Proof.
   intros ? j; destruct (decide (i = j)) as [->|].
-  * rewrite lookup_insert. destruct (m !! j); eauto.
-  * rewrite lookup_insert_ne by done. by destruct (m !! j).
+  * rewrite lookup_insert. destruct (m !! j); simpl; eauto.
+  * rewrite lookup_insert_ne by done. by destruct (m !! j); simpl.
 Qed.
 Lemma insert_subseteq {A} (m : M A) i x : m !! i = None → m ⊆ <[i:=x]>m.
 Proof. apply partial_alter_subseteq. Qed.
@@ -465,6 +522,17 @@ Proof.
   * by rewrite lookup_omap, !lookup_singleton.
   * by rewrite lookup_omap, !lookup_singleton_ne.
 Qed.
+Lemma map_fmap_id {A} (m : M A) : id <$> m = m.
+Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
+Lemma map_fmap_compose {A B C} (f : A → B) (g : B → C) (m : M A) :
+  g ∘ f <$> m = g <$> f <$> m.
+Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed.
+Lemma map_fmap_ext {A B} (f1 f2 : A → B) m :
+  (∀ i x, m !! i = Some x → f1 x = f2 x) → f1 <$> m = f2 <$> m.
+Proof.
+  intros Hi; apply map_eq; intros i; rewrite !lookup_fmap.
+  by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto.
+Qed.
 
 (** ** Properties of conversion to lists *)
 Lemma map_to_list_unique {A} (m : M A) i x y :
@@ -807,7 +875,7 @@ Lemma insert_merge_r m1 m2 i x z :
 Proof. by intros; apply partial_alter_merge_r. Qed.
 End more_merge.
 
-(** ** Properties on the [map_Forall2] relation *)
+(** ** Properties on the [map_relation] relation *)
 Section Forall2.
 Context {A B} (R : A → B → Prop) (P : A → Prop) (Q : B → Prop).
 Context `{∀ x y, Decision (R x y), ∀ x, Decision (P x), ∀ y, Decision (Q y)}.
@@ -819,8 +887,8 @@ Let f (mx : option A) (my : option B) : option bool :=
   | None, Some y => Some (bool_decide (Q y))
   | None, None => None
   end.
-Lemma map_Forall2_alt (m1 : M A) (m2 : M B) :
-  map_Forall2 R P Q m1 m2 ↔ map_Forall (λ _, Is_true) (merge f m1 m2).
+Lemma map_relation_alt (m1 : M A) (m2 : M B) :
+  map_relation R P Q m1 m2 ↔ map_Forall (λ _, Is_true) (merge f m1 m2).
 Proof.
   split.
   * intros Hm i P'; rewrite lookup_merge by done; intros.
@@ -830,71 +898,72 @@ Proof.
     destruct (m1 !! i), (m2 !! i); simplify_equality'; auto;
       by eapply bool_decide_unpack, Hm.
 Qed.
-Global Instance map_Forall2_dec `{∀ x y, Decision (R x y), ∀ x, Decision (P x),
-  ∀ y, Decision (Q y)} m1 m2 : Decision (map_Forall2 R P Q m1 m2).
+Global Instance map_relation_dec `{∀ x y, Decision (R x y), ∀ x, Decision (P x),
+  ∀ y, Decision (Q y)} m1 m2 : Decision (map_relation R P Q m1 m2).
 Proof.
   refine (cast_if (decide (map_Forall (λ _, Is_true) (merge f m1 m2))));
-    abstract by rewrite map_Forall2_alt.
+    abstract by rewrite map_relation_alt.
 Defined.
 (** Due to the finiteness of finite maps, we can extract a witness if the
 relation does not hold. *)
 Lemma map_not_Forall2 (m1 : M A) (m2 : M B) :
-  ¬map_Forall2 R P Q m1 m2 ↔ ∃ i,
+  ¬map_relation R P Q m1 m2 ↔ ∃ i,
     (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ ¬R x y)
     ∨ (∃ x, m1 !! i = Some x ∧ m2 !! i = None ∧ ¬P x)
     ∨ (∃ y, m1 !! i = None ∧ m2 !! i = Some y ∧ ¬Q y).
 Proof.
   split.
-  * rewrite map_Forall2_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i.
+  * rewrite map_relation_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i.
     rewrite lookup_merge in Hm by done.
     destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack.
-  * by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm;
+  * unfold map_relation, option_relation.
+    by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm;
       specialize (Hm i); simplify_option_equality.
 Qed.
 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].
   intros [i[(x&y&?&?&?)|[(x&?&?&[])|(y&?&?&[])]]]; naive_solver.
 Qed.
-Global Instance: Symmetric (@disjoint (M A) _).
+Global Instance: 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.
-Proof. rewrite (symmetry_iff (⊥)). apply map_disjoint_Some_l. Qed.
-Lemma map_disjoint_singleton_l {A} (m : M A) i x : {[i, x]} ⊥ m ↔ m !! 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.
 Proof.
   split; [|rewrite !map_disjoint_spec].
   * intro. apply (map_disjoint_Some_l {[i, x]} _ _ x);
@@ -904,20 +973,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.
-Proof. by rewrite (symmetry_iff (⊥)), map_disjoint_singleton_l. Qed.
+  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 *)
@@ -1036,7 +1105,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.
@@ -1045,9 +1114,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_commutative {A} (m1 m2 : M A) : m1 ⊥ m2 → m1 ∪ m2 = m2 ∪ m1.
+Lemma map_union_commutative {A} (m1 m2 : M A) : m1 ⊥ₘ m2 → m1 ∪ m2 = m2 ∪ m1.
 Proof.
   intros Hdisjoint. apply (merge_commutative (union_with (λ x _, Some x))).
   intros i. specialize (Hdisjoint i).
@@ -1065,14 +1134,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_commutative 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. transitivity 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. transitivity m3; auto using map_union_subseteq_r. Qed.
 Lemma map_union_preserving_l {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m3 ∪ m1 ⊆ m3 ∪ m2.
 Proof.
@@ -1080,52 +1149,52 @@ Proof.
   rewrite !lookup_union_Some_raw. naive_solver.
 Qed.
 Lemma map_union_preserving_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_commutative _ m3)
     by eauto using map_disjoint_weaken_l.
   by apply map_union_preserving_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_commutative _ 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_symmetric (⊆));
     apply map_union_reflecting_l with m3; auto using (reflexive_eq (R:=(⊆))).
 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_symmetric (⊆));
     apply map_union_reflecting_r with m3; auto using (reflexive_eq (R:=(⊆))).
 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.
@@ -1142,22 +1211,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.
@@ -1181,7 +1250,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.
@@ -1189,23 +1258,14 @@ 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.
-Proof. by rewrite (symmetry_iff (⊥)), map_disjoint_union_list_l. Qed.
+  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.
-Lemma map_union_sublist {A} (ms1 ms2 : list (M A)) :
-  ⊥ ms2 → ms1 `sublist` ms2 → ⋃ ms1 ⊆ ⋃ ms2.
-Proof.
-  intros Hms2. revert ms1.
-  induction Hms2 as [|m2 ms2]; intros ms1; [by inversion 1|].
-  rewrite sublist_cons_r. intros [?|(ms1' &?&?)]; subst; simpl.
-  * transitivity (⋃ ms2); auto. by apply map_union_subseteq_r.
-  * apply map_union_preserving_l; auto.
-Qed.
 
 (** ** Properties of the folding the [delete] function *)
 Lemma lookup_foldr_delete {A} (m : M A) is j :
@@ -1231,10 +1291,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.
@@ -1242,7 +1302,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.
@@ -1250,48 +1310,30 @@ 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.
-Proof. by rewrite (symmetry_iff (⊥)), map_disjoint_of_list_l. Qed.
+  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.
-Proof. intro. by rewrite (symmetry_iff (⊥)), map_disjoint_of_list_zip_l. Qed.
+  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 with respect to vectors *)
-Lemma union_delete_vec {A n} (ms : vec (M A) n) (i : fin n) :
-  ⊥ ms → ms !!! i ∪ ⋃ delete (fin_to_nat i) (vec_to_list ms) = ⋃ ms.
-Proof.
-  induction ms as [|m ? ms IH]; inversion_clear 1; inv_fin i; simpl; auto.
-  intros i. rewrite (map_union_commutative m), (associative_L (∪)), IH.
-  * by rewrite map_union_commutative.
-  * done.
-  * apply map_disjoint_weaken_r with (⋃ ms); [done |].
-    apply map_union_sublist; auto using sublist_delete.
-Qed.
-Lemma union_insert_vec {A n} (ms : vec (M A) n) (i : fin n) m :
-  m ⊥ ⋃ delete (fin_to_nat i) (vec_to_list ms) →
-  ⋃ vinsert i m ms = m ∪ ⋃ delete (fin_to_nat i) (vec_to_list ms).
-Proof.
-  induction ms as [|m' ? ms IH]; inv_fin i; simpl; [done | intros i Hdisjoint].
-  rewrite map_disjoint_union_r in Hdisjoint.
-  rewrite IH, !(associative_L (∪)), (map_union_commutative m); intuition.
-Qed.
-
 (** ** Properties of the [intersection_with] operation *)
 Lemma lookup_intersection_with {A} (f : A → A → option A) m1 m2 i :
   intersection_with f m1 m2 !! i = intersection_with f (m1 !! i) (m2 !! i).
@@ -1344,13 +1386,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.
@@ -1372,23 +1414,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 : ⊥ [] |- _ => clear H
-  | H : ⊥ [_] |- _ => clear H
-  | H : ⊥ (_ :: _) |- _ => apply disjoint_list_cons in H; destruct 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
@@ -1399,30 +1438,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 disjoint_nil_2 : map_disjoint.
-Hint Extern 2 (⊥ (_ :: _)) => apply disjoint_cons_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
diff --git a/theories/option.v b/theories/option.v
index d41b35ddf359b720db3bb482195b20e52925a029..a67260f46c918ef0a0d92701e03dd42435e6a6e3 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -74,6 +74,40 @@ Proof. destruct x; unfold is_Some; naive_solver. Qed.
 Lemma not_eq_None_Some `(x : option A) : x ≠ None ↔ is_Some x.
 Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed.
 
+(** Lifting a relation point-wise to option *)
+Inductive option_Forall2 {A B} (P: A → B → Prop) : option A → option B → Prop :=
+  | Some_Forall2 x y : P x y → option_Forall2 P (Some x) (Some y)
+  | None_Forall2 : option_Forall2 P None None.
+Definition option_relation {A B} (R: A → B → Prop) (P: A → Prop) (Q: B → Prop)
+    (mx : option A) (my : option B) : Prop :=
+  match mx, my with
+  | Some x, Some y => R x y
+  | Some x, None => P x
+  | None, Some y => Q y
+  | None, None => True
+  end.
+
+(** Setoids *)
+Section setoids.
+  Context `{Equiv A}.
+  Global Instance option_equiv : Equiv (option A) := option_Forall2 (≡).
+  Global Instance option_equivalence `{!Equivalence ((≡) : relation A)} :
+    Equivalence ((≡) : relation (option A)).
+  Proof.
+    split.
+    * by intros []; constructor.
+    * by destruct 1; constructor.
+    * destruct 1; inversion 1; constructor; etransitivity; eauto.
+  Qed.
+  Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A).
+  Proof. by constructor. Qed.
+  Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
+  Proof.
+    intros x y; split; [destruct 1; fold_leibniz; congruence|].
+    by intros <-; destruct x; constructor; fold_leibniz.
+  Qed.
+End setoids.
+
 (** Equality on [option] is decidable. *)
 Instance option_eq_None_dec {A} (x : option A) : Decision (x = None) :=
   match x with Some _ => right (Some_ne_None _) | None => left eq_refl end.
diff --git a/theories/prelude.v b/theories/prelude.v
index 75e7d67262788fd6f6b82c9c84e082812f25b8b1..0c00f512508add9f675a56174ec66706eedae65f 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -8,7 +8,7 @@ Require Export
   option
   vector
   numbers
-  ars
+  relations
   collections
   fin_collections
   listset
diff --git a/theories/pretty.v b/theories/pretty.v
index 86e4b47effdd4bce01b9da3c6de5c367a017382b..2bd7f21d685547ab973338a6bba9ee974c5a3b7c 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -1,7 +1,7 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 Require Export numbers option.
-Require Import Ascii String ars.
+Require Import Ascii String relations.
 
 Infix "+:+" := String.append (at level 60, right associativity) : C_scope.
 Arguments String.append _ _ : simpl never.
diff --git a/theories/ars.v b/theories/relations.v
similarity index 97%
rename from theories/ars.v
rename to theories/relations.v
index 0b422b990609d48e13e41ab61767120c04560666..da9523984bda004747e021bacb66f56b56925e0e 100644
--- a/theories/ars.v
+++ b/theories/relations.v
@@ -22,6 +22,11 @@ Section definitions.
     | rtc_refl x : rtc x x
     | rtc_l x y z : R x y → rtc y z → rtc x z.
 
+  (** The reflexive transitive closure for setoids. *)
+  Inductive rtcS `{Equiv A} : relation A :=
+    | rtcS_refl x y : x ≡ y → rtcS x y
+    | rtcS_l x y z : R x y → rtcS y z → rtcS x z.
+
   (** Reductions of exactly [n] steps. *)
   Inductive nsteps : nat → relation A :=
     | nsteps_O x : nsteps 0 x x
diff --git a/theories/sets.v b/theories/sets.v
new file mode 100644
index 0000000000000000000000000000000000000000..9e3d2d210d210d6e262e7ed360b490d931e7943b
--- /dev/null
+++ b/theories/sets.v
@@ -0,0 +1,31 @@
+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file implements sets as functions into Prop. *)
+Require Export prelude.
+
+Record set (A : Type) : Type := mkSet { set_car : A → Prop }.
+Arguments mkSet {_} _.
+Arguments set_car {_} _ _.
+Definition set_all {A} : set A := mkSet (λ _, True).
+Instance set_empty {A} : Empty (set A) := mkSet (λ _, False).
+Instance set_singleton {A} : Singleton A (set A) := λ x, mkSet (x =).
+Instance set_elem_of {A} : ElemOf A (set A) := λ x X, set_car X x.
+Instance set_union {A} : Union (set A) := λ X1 X2, mkSet (λ x, x ∈ X1 ∨ x ∈ X2).
+Instance set_intersection {A} : Intersection (set A) := λ X1 X2,
+  mkSet (λ x, x ∈ X1 ∧ x ∈ X2).
+Instance set_difference {A} : Difference (set A) := λ X1 X2,
+  mkSet (λ x, x ∈ X1 ∧ x ∉ X2).
+Instance set_collection : Collection A (set A).
+Proof. by split; [split | |]; repeat intro. Qed.
+
+Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
+Instance set_bind : MBind set := λ A B (f : A → set B) (X : set A),
+  mkSet (λ b, ∃ a, b ∈ f a ∧ a ∈ X).
+Instance set_fmap : FMap set := λ A B (f : A → B) (X : set A),
+  mkSet (λ b, ∃ a, b = f a ∧ a ∈ X).
+Instance set_join : MJoin set := λ A (XX : set (set A)),
+  mkSet (λ a, ∃ X, a ∈ X ∧ X ∈ XX).
+Instance set_collection_monad : CollectionMonad set.
+Proof. by split; try apply _. Qed.
+
+Global Opaque set_union set_intersection.
\ No newline at end of file
diff --git a/theories/tactics.v b/theories/tactics.v
index 73c0e9dbf840dba017f6c534d7a599d70d93cfd5..70f4f94120ef13483dbbe32604226c0422c0f910 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -207,6 +207,26 @@ Ltac f_lia :=
   end.
 Ltac f_lia' := csimpl in *; f_lia.
 
+Ltac setoid_subst_l x :=
+  match goal with
+  | H : x ≡ ?y |- _ =>
+     is_var x;
+     try match y with x _ => fail 2 end;
+     repeat match goal with
+     | |- context [ x ] => setoid_rewrite H
+     | H' : context [ x ] |- _ =>
+        try match H' with H => fail 2 end;
+        setoid_rewrite H in H'
+     end;
+     clear H
+  end.
+Ltac setoid_subst :=
+  repeat match goal with
+  | _ => progress simplify_equality'
+  | H : ?x ≡ _ |- _ => setoid_subst_l x
+  | H : _ ≡ ?x |- _ => symmetry in H; setoid_subst_l x
+  end.
+
 (** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2]
 runs [tac x] for each element [x] until [tac x] succeeds. If it does not
 suceed for any element of the generated list, the whole tactic wil fail. *)