From 50dfc1488f5f92bfde5dd20cd0d119ce61f5fb63 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 12 Nov 2012 13:44:48 +0100
Subject: [PATCH] Many relatively small changes.

Most interestingly:
* Use [lia] instead of [omega] everywhere
* More many generic lemmas on the memory to the theory on finite maps.
* Many additional list lemmas.
* A new interface for a monad for collections, which is now also used by the
  collection tactics.
* Provide an additional finite collection implementation using unordered lists
  without duplicates removed. This implementation forms a monad (just the list
  monad in disguise).
---
 theories/ars.v             |   10 +-
 theories/base.v            |  204 ++++--
 theories/collections.v     |  162 +++--
 theories/decidable.v       |    8 +-
 theories/fin_collections.v |   72 +-
 theories/fin_maps.v        | 1295 +++++++++++++++++++++++++-----------
 theories/fresh_numbers.v   |    9 +-
 theories/list.v            | 1280 +++++++++++++++++++++++++----------
 theories/listset.v         |  181 ++---
 theories/nmap.v            |   34 +-
 theories/numbers.v         |   87 +++
 theories/option.v          |   68 +-
 theories/orders.v          |    3 +-
 theories/pmap.v            |   68 +-
 theories/prelude.v         |    6 +-
 theories/subset.v          |   19 -
 theories/tactics.v         |   13 +
 theories/vector.v          |   11 +-
 18 files changed, 2431 insertions(+), 1099 deletions(-)
 delete mode 100644 theories/subset.v

diff --git a/theories/ars.v b/theories/ars.v
index d56f995a..8cbb24b5 100644
--- a/theories/ars.v
+++ b/theories/ars.v
@@ -4,7 +4,7 @@
 These are particularly useful as we define the operational semantics as a
 small step semantics. This file defines a hint database [ars] containing
 some theorems on abstract rewriting systems. *)
-Require Import Omega Wf_nat.
+Require Import Wf_nat.
 Require Export tactics base.
 
 (** * Definitions *)
@@ -101,7 +101,7 @@ Section rtc.
     bsteps R n x y → bsteps R (m + n) x y.
   Proof. apply bsteps_weaken. auto with arith. Qed.
   Lemma bsteps_S n x y :  bsteps R n x y → bsteps R (S n) x y.
-  Proof. apply bsteps_weaken. omega. Qed.
+  Proof. apply bsteps_weaken. lia. Qed.
   Lemma bsteps_trans n m x y z :
     bsteps R n x y → bsteps R m y z → bsteps R (n + m) x z.
   Proof. induction 1; simpl; eauto using bsteps_plus_l with ars. Qed.
@@ -129,11 +129,11 @@ Section rtc.
     induction 1 as [|m x' y z p2 p3 IH]; [by eauto with arith|].
     intros n p1 H. rewrite <-plus_n_Sm.
     apply (IH (S n)); [by eauto using bsteps_r |].
-    intros [|m'] [??]; [omega |].
+    intros [|m'] [??]; [lia |].
     apply Pstep with x'.
-    * apply bsteps_weaken with n; intuition omega.
+    * apply bsteps_weaken with n; intuition lia.
     * done.
-    * apply H; intuition omega.
+    * apply H; intuition lia.
   Qed.
 
   Global Instance tc_trans: Transitive (tc R).
diff --git a/theories/base.v b/theories/base.v
index 7b027c68..4ddd3a76 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -177,15 +177,74 @@ Notation "(⊥)" := disjoint (only parsing) : C_scope.
 Notation "( X ⊥)" := (disjoint X) (only parsing) : C_scope.
 Notation "(⊥ X )" := (λ Y, disjoint Y X) (only parsing) : C_scope.
 
+Inductive list_disjoint `{Disjoint A} : list A → Prop :=
+  | disjoint_nil :
+     list_disjoint []
+  | disjoint_cons X Xs :
+     Forall (⊥ X) Xs →
+     list_disjoint Xs →
+     list_disjoint (X :: Xs).
+Lemma list_disjoint_cons_inv `{Disjoint A} X Xs :
+  list_disjoint (X :: Xs) →
+  Forall (⊥ X) Xs ∧ list_disjoint Xs.
+Proof. inversion_clear 1; auto. Qed.
+
 Instance generic_disjoint `{ElemOf A B} : Disjoint B | 100 :=
   λ X Y, ∀ x, x ∉ X ∨ x ∉ Y.
 
+(** ** Monadic operations *)
+(** We define operational type classes for the monadic operations bind, join 
+and fmap. These type classes are defined in a non-standard way by taking the
+function as a parameter of the class. For example, we define
+<<
+  Class FMapD := fmap: ∀ {A B}, (A → B) → M A → M B.
+>>
+instead of
+<<
+  Class FMap {A B} (f : A → B) := fmap: M A → M B.
+>>
+This approach allows us to define [fmap] on lists such that [simpl] unfolds it
+in the appropriate way, and so that it can be used for mutual recursion
+(the mapped function [f] is not part of the fixpoint) as well. This is a hack,
+and should be replaced by something more appropriate in future versions. *)
+
+(* We use these type classes merely for convenient overloading of notations and
+do not formalize any theory on monads (we do not even define a class with the
+monad laws). *)
+Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A.
+Instance: Params (@mret) 3.
+Arguments mret {_ _ _} _.
+
+Class MBindD (M : Type → Type) {A B} (f : A → M B) := mbind: M A → M B.
+Notation MBind M := (∀ {A B} (f : A → M B), MBindD M f)%type.
+Instance: Params (@mbind) 5.
+Arguments mbind {_ _ _} _ {_} !_ / : simpl nomatch.
+
+Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A.
+Instance: Params (@mjoin) 3.
+Arguments mjoin {_ _ _} !_ / : simpl nomatch.
+
+Class FMapD (M : Type → Type) {A B} (f : A → B) := fmap: M A → M B.
+Notation FMap M := (∀ {A B} (f : A → B), FMapD M f)%type.
+Instance: Params (@fmap) 6.
+Arguments fmap {_ _ _} _ {_} !_ / : simpl nomatch.
+
+Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
+Notation "x ← y ; z" := (y ≫= (λ x : _, z))
+  (at level 65, only parsing, next at level 35, right associativity) : C_scope.
+Infix "<$>" := fmap (at level 65, right associativity, only parsing) : C_scope.
+
+Class MGuard (M : Type → Type) :=
+  mguard: ∀ P {dec : Decision P} {A}, M A → M A.
+Notation "'guard' P ; o" := (mguard P o)
+  (at level 65, only parsing, next at level 35, right associativity) : C_scope.
+
 (** ** Operations on maps *)
 (** In this section we define operational type classes for the operations
 on maps. In the file [fin_maps] we will axiomatize finite maps.
 The function lookup [m !! k] should yield the element at key [k] in [m]. *)
-Class Lookup (K : Type) (M : Type → Type) :=
-  lookup: ∀ {A}, K → M A → option A.
+Class Lookup (K M A : Type) :=
+  lookup: K → M → option A.
 Instance: Params (@lookup) 4.
 
 Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
@@ -196,8 +255,8 @@ Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
 
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
-Class Insert (K : Type) (M : Type → Type) :=
-  insert: ∀ {A}, K → A → M A → M A.
+Class Insert (K M A : Type) :=
+  insert: K → A → M → M.
 Instance: Params (@insert) 4.
 Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
@@ -206,33 +265,34 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch.
 (** The function delete [delete k m] should delete the value at key [k] in
 [m]. If the key [k] is not a member of [m], the original map should be
 returned. *)
-Class Delete (K : Type) (M : Type → Type) :=
-  delete: ∀ {A}, K → M A → M A.
-Instance: Params (@delete) 4.
-Arguments delete _ _ _ _ !_ !_ / : simpl nomatch.
+Class Delete (K M : Type) :=
+  delete: K → M → M.
+Instance: Params (@delete) 3.
+Arguments delete _ _ _ !_ !_ / : simpl nomatch.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value. *)
-Class Alter (K : Type) (M : Type → Type) :=
-  alter: ∀ {A}, (A → A) → K → M A → M A.
-Instance: Params (@alter) 4.
-Arguments alter _ _ _ _ _ !_ !_ / : simpl nomatch.
+Class AlterD (K M A : Type) (f : A → A) :=
+  alter: K → M → M.
+Notation Alter K M A := (∀ (f : A → A), AlterD K M A f)%type.
+Instance: Params (@alter) 5.
+Arguments alter {_ _ _} _ {_} !_ !_ / : simpl nomatch.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value at key [k] or [None]
 if [k] is not a member of [m]. The value at [k] should be deleted if [f] 
 yields [None]. *)
-Class PartialAlter (K : Type) (M : Type → Type) :=
-  partial_alter: ∀ {A}, (option A → option A) → K → M A → M A.
+Class PartialAlter (K M A : Type) :=
+  partial_alter: (option A → option A) → K → M → M.
 Instance: Params (@partial_alter) 4.
 Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
 
 (** The function [dom C m] should yield the domain of [m]. That is a finite
 collection of type [C] that contains the keys that are a member of [m]. *)
-Class Dom (K : Type) (M : Type → Type) :=
-  dom: ∀ {A} C `{Empty C} `{Union C} `{Singleton K C}, M A → C.
-Instance: Params (@dom) 8.
-Arguments dom _ _ _ _ _ _ _ _ !_ / : simpl nomatch.
+Class Dom (K M : Type) :=
+  dom: ∀ C `{Empty C} `{Union C} `{Singleton K C}, M → C.
+Instance: Params (@dom) 7.
+Arguments dom _ _ _ _ _ _ _ !_ / : simpl nomatch.
 
 (** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
 constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)]
@@ -243,12 +303,17 @@ Instance: Params (@merge) 3.
 Arguments merge _ _ _ _ !_ !_ / : simpl nomatch.
 
 (** We lift the insert and delete operation to lists of elements. *)
-Definition insert_list `{Insert K M} {A} (l : list (K * A)) (m : M A) : M A :=
+Definition insert_list `{Insert K M A} (l : list (K * A)) (m : M) : M :=
   fold_right (λ p, <[ fst p := snd p ]>) m l.
 Instance: Params (@insert_list) 4.
-Definition delete_list `{Delete K M} {A} (l : list K) (m : M A) : M A :=
+Definition delete_list `{Delete K M} (l : list K) (m : M) : M :=
   fold_right delete m l.
-Instance: Params (@delete_list) 4.
+Instance: Params (@delete_list) 3.
+
+Definition insert_consecutive `{Insert nat M A}
+    (i : nat) (l : list A) (m : M) : M :=
+  fold_right (λ x f i, <[i:=x]>(f (S i))) (λ _, m) l i.
+Instance: Params (@insert_consecutive) 3.
 
 (** The function [union_with f m1 m2] should yield the union of [m1] and [m2]
 using the function [f] to combine values of members that are in both [m1] and
@@ -320,43 +385,6 @@ Lemma right_absorb_eq {A} (i : A) (f : A → A → A) `{!RightAbsorb (=) i f} x
   f x i = i.
 Proof. auto. Qed.
 
-(** ** Monadic operations *)
-(** We define operational type classes for the monadic operations bind, join 
-and fmap. These type classes are defined in a non-standard way by taking the
-function as a parameter of the class. For example, we define
-<<
-  Class FMap := fmap: ∀ {A B}, (A → B) → M A → M B.
->>
-instead of
-<<
-  Class FMap {A B} (f : A → B) := fmap: M A → M B.
->>
-This approach allows us to define [fmap] on lists such that [simpl] unfolds it
-in the appropriate way, and so that it can be used for mutual recursion
-(the mapped function [f] is not part of the fixpoint) as well.
-We use these type classes merely for convenient overloading of notations and do
-not formalize any theory on monads (we do not even define a class with the
-monad laws). *)
-Section monad_ops.
-  Context (M : Type → Type).
-
-  Class MBind {A B} (f : A → M B) := mbind: M A → M B.
-  Class MJoin {A} := mjoin: M (M A) → M A.
-  Class FMap {A B} (f : A → B) := fmap: M A → M B.
-End monad_ops.
-
-Instance: Params (@mbind) 4.
-Arguments mbind {_ _ _} _ {_} !_ / : simpl nomatch.
-Instance: Params (@mjoin) 3.
-Arguments mjoin {_ _ _} !_ / : simpl nomatch.
-Instance: Params (@fmap) 4.
-Arguments fmap {_ _ _} _ {_} !_ / : simpl nomatch.
-
-Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
-Notation "x ← y ; z" := (y ≫= (λ x : _, z))
-  (at level 65, next at level 35, right associativity) : C_scope.
-Infix "<$>" := fmap (at level 65, right associativity, only parsing) : C_scope.
-
 (** ** Axiomatization of ordered structures *)
 (** A pre-order equiped with a smallest element. *)
 Class BoundedPreOrder A `{Empty A} `{SubsetEq A} := {
@@ -386,19 +414,20 @@ Class LowerBoundedLattice A `{Empty A} `{SubsetEq A}
   lbl_msl :>> MeetSemiLattice A
 }.
 (** ** Axiomatization of collections *)
-(** The class [Collection A C] axiomatizes a collection of type [C] with
-elements of type [A]. Since [C] is not dependent on [A], we use the monomorphic
-[Map] type class instead of the polymorphic [FMap]. *)
-Class Map A C := map: (A → A) → (C → C).
+(** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
+elements of type [A]. *)
 Instance: Params (@map) 3.
-Class Collection A C `{ElemOf A C} `{Empty C} `{Union C}
-    `{Intersection C} `{Difference C} `{Singleton A C} `{Map A C} := {
+Class SimpleCollection A C `{ElemOf A C}
+  `{Empty C} `{Singleton A C} `{Union C} := {
   not_elem_of_empty (x : A) : x ∉ ∅;
   elem_of_singleton (x y : A) : x ∈ {[ y ]} ↔ x = y;
-  elem_of_union X Y (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y;
+  elem_of_union X Y (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y
+}.
+Class Collection A C `{ElemOf A C} `{Empty C} `{Singleton A C} `{Union C}
+    `{Intersection C} `{Difference C} := {
+  collection_simple :>> SimpleCollection A C;
   elem_of_intersection X Y (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
-  elem_of_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y;
-  elem_of_map f X (x : A) : x ∈ map f X ↔ ∃ y, x = f y ∧ y ∈ X
+  elem_of_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
 }.
 
 (** We axiomative a finite collection as a collection whose elements can be
@@ -407,24 +436,59 @@ in any order and should not contain duplicates. *)
 Class Elements A C := elements: C → list A.
 Instance: Params (@elements) 3.
 
+(** We redefine the standard library's [In] and [NoDup] using type classes. *)
+Inductive elem_of_list {A} : ElemOf A (list A) :=
+  | elem_of_list_here (x : A) l : x ∈ x :: l
+  | elem_of_list_further (x y : A) l : x ∈ l → x ∈ y :: l.
+Existing Instance elem_of_list.
+
+Inductive NoDup {A} : list A → Prop :=
+  | NoDup_nil_2 : NoDup []
+  | NoDup_cons_2 x l : x ∉ l → NoDup l → NoDup (x :: l).
+
 (** Decidability of equality of the carrier set is admissible, but we add it
 anyway so as to avoid cycles in type class search. *)
 Class FinCollection A C `{ElemOf A C} `{Empty C} `{Union C}
-    `{Intersection C} `{Difference C} `{Singleton A C} `{Map A C}
+    `{Intersection C} `{Difference C} `{Singleton A C}
     `{Elements A C} `{∀ x y : A, Decision (x = y)} := {
   fin_collection :>> Collection A C;
-  elements_spec X x : x ∈ X ↔ In x (elements X);
+  elements_spec X x : x ∈ X ↔ x ∈ elements X;
   elements_nodup X : NoDup (elements X)
 }.
 Class Size C := size: C → nat.
+Arguments size {_ _} !_ / : simpl nomatch.
 Instance: Params (@size) 2.
 
+(** The class [Collection M] axiomatizes a type constructor [M] that can be
+used to construct a collection [M A] with elements of type [A]. The advantage
+of this class, compared to [Collection], is that it also axiomatizes the
+the monadic operations. The disadvantage, is that not many inhabits are
+possible (we will only provide an inhabitant using unordered lists without
+duplicates removed). More interesting implementations typically need
+decidability of equality, or a total order on the elements, which do not fit
+in a type constructor of type [Type → Type]. *)
+Class CollectionMonad M `{∀ A, ElemOf A (M A)}
+    `{∀ A, Empty (M A)} `{∀ A, Singleton A (M A)} `{∀ A, Union (M A)}
+    `{!MBind M} `{!MRet M} `{!FMap M} `{!MJoin M} := {
+  collection_monad_simple A :> SimpleCollection A (M A);
+  elem_of_bind {A B} (f : A → M B) (x : B) (X : M A) :
+    x ∈ X ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ X;
+  elem_of_ret {A} (x y : A) :
+    x ∈ mret y ↔ x = y;
+  elem_of_fmap {A B} (f : A → B) (x : B) (X : M A) :
+    x ∈ f <$> X ↔ ∃ y, x = f y ∧ y ∈ X;
+  elem_of_join {A} (x : A) (X : M (M A)) :
+    x ∈ mjoin X ↔ ∃ Y, x ∈ Y ∧ Y ∈ X
+}.
+
 (** The function [fresh X] yields an element that is not contained in [X]. We
 will later prove that [fresh] is [Proper] with respect to the induced setoid
 equality on collections. *)
 Class Fresh A C := fresh: C → A.
 Instance: Params (@fresh) 3.
-Class FreshSpec A C `{!Fresh A C} `{!ElemOf A C} := {
+Class FreshSpec A C `{ElemOf A C}
+    `{Empty C} `{Singleton A C} `{Union C} `{Fresh A C} := {
+  fresh_collection_simple :>> SimpleCollection A C;
   fresh_proper_alt X Y : (∀ x, x ∈ X ↔ x ∈ Y) → fresh X = fresh Y;
   is_fresh (X : C) : fresh X ∉ X
 }.
diff --git a/theories/collections.v b/theories/collections.v
index cb90c53f..9013df37 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -6,8 +6,8 @@ collections. *)
 Require Export base tactics orders.
 
 (** * Theorems *)
-Section collection.
-  Context `{Collection A C}.
+Section simple_collection.
+  Context `{SimpleCollection A C}.
 
   Lemma elem_of_empty x : x ∈ ∅ ↔ False.
   Proof. split. apply not_elem_of_empty. done. Qed.
@@ -18,7 +18,7 @@ Section collection.
 
   Global Instance collection_subseteq: SubsetEq C := λ X Y,
     ∀ x, x ∈ X → x ∈ Y.
-  Global Instance: LowerBoundedLattice C.
+  Global Instance: BoundedJoinSemiLattice C.
   Proof. firstorder auto. Qed.
 
   Lemma elem_of_subseteq X Y : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y.
@@ -36,28 +36,25 @@ Section collection.
   Qed.
   Global Instance singleton_proper : Proper ((=) ==> (≡)) singleton.
   Proof. repeat intro. by subst. Qed.
-  Global Instance elem_of_proper: Proper ((=) ==> (≡) ==> iff) (∈).
+  Global Instance elem_of_proper: Proper ((=) ==> (≡) ==> iff) (∈) | 5.
   Proof. intros ???. subst. firstorder. Qed.
 
   Lemma elem_of_union_list (x : A) (Xs : list C) :
-    x ∈ ⋃ Xs ↔ ∃ X, In X Xs ∧ x ∈ X.
+    x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
   Proof.
     split.
     * induction Xs; simpl; intros HXs.
       + by apply elem_of_empty in HXs.
-      + apply elem_of_union in HXs. naive_solver.
-    * intros [X []]. induction Xs; [done | intros [?|?] ?; subst; simpl].
+      + setoid_rewrite elem_of_cons.
+        apply elem_of_union in HXs. naive_solver.
+    * intros [X []]. induction 1; simpl.
       + by apply elem_of_union_l.
-      + apply elem_of_union_r; auto.
+      + intros. apply elem_of_union_r; auto.
   Qed.
 
   Lemma non_empty_singleton x : {[ x ]} ≢ ∅.
   Proof. intros [E _]. by apply (elem_of_empty x), E, elem_of_singleton. Qed.
 
-  Lemma intersection_twice x : {[x]} ∩ {[x]} ≡ {[x]}.
-  Proof.
-    split; intros y; rewrite elem_of_intersection, !elem_of_singleton; tauto.
-  Qed.
   Lemma not_elem_of_singleton x y : x ∉ {[ y ]} ↔ x ≠ y.
   Proof. by rewrite elem_of_singleton. Qed.
   Lemma not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
@@ -70,6 +67,20 @@ Section collection.
     refine (cast_if (decide_rel (⊆) {[ x ]} X));
       by rewrite elem_of_subseteq_singleton.
   Defined.
+End simple_collection.
+
+Section collection.
+  Context `{Collection A C}.
+
+  Global Instance: LowerBoundedLattice C.
+  Proof. split. apply _. firstorder auto. Qed.
+
+  Lemma intersection_twice x : {[x]} ∩ {[x]} ≡ {[x]}.
+  Proof.
+    split; intros y; rewrite elem_of_intersection, !elem_of_singleton; tauto.
+  Qed.
+
+  Context `{∀ (X Y : C), Decision (X ⊆ Y)}.
 
   Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
   Proof.
@@ -96,21 +107,6 @@ Ltac decompose_empty := repeat
   | H : {[ _ ]} ≡ ∅ |- _ => destruct (non_empty_singleton _ H)
   end.
 
-(** * Theorems about map *)
-Section map.
-  Context `{Collection A C}.
-
-  Lemma elem_of_map_1 (f : A → A) (X : C) (x : A) :
-    x ∈ map f X → ∃ y, x = f y ∧ y ∈ X.
-  Proof. intros. by apply (elem_of_map _). Qed.
-  Lemma elem_of_map_2 (f : A → A) (X : C) (x : A) :
-    x ∈ X → f x ∈ map f X.
-  Proof. intros. apply (elem_of_map _). eauto. Qed.
-  Lemma elem_of_map_2_alt (f : A → A) (X : C) (x : A) y :
-    x ∈ X → y = f x → y ∈ map f X.
-  Proof. intros. apply (elem_of_map _). eauto. Qed.
-End map.
-
 (** * Tactics *)
 (** The first pass consists of eliminating all occurrences of [(∪)], [(∩)],
 [(∖)], [map], [∅], [{[_]}], [(≡)], and [(⊆)], by rewriting these into
@@ -126,7 +122,10 @@ Ltac unfold_elem_of :=
     | context [ _ ∈ _ ∪ _ ] => setoid_rewrite elem_of_union in H
     | context [ _ ∈ _ ∩ _ ] => setoid_rewrite elem_of_intersection in H
     | context [ _ ∈ _ ∖ _ ] => setoid_rewrite elem_of_difference in H
-    | context [ _ ∈ map _ _ ] => setoid_rewrite elem_of_map in H
+    | context [ _ ∈ _ <$> _ ] => setoid_rewrite elem_of_fmap in H
+    | context [ _ ∈ mret _ ] => setoid_rewrite elem_of_ret in H
+    | context [ _ ∈ _ ≫= _ ] => setoid_rewrite elem_of_bind in H
+    | context [ _ ∈ mjoin _ ] => setoid_rewrite elem_of_join in H
     end);
   repeat match goal with
   | |- context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq
@@ -136,7 +135,10 @@ Ltac unfold_elem_of :=
   | |- context [ _ ∈ _ ∪ _ ] => setoid_rewrite elem_of_union
   | |- context [ _ ∈ _ ∩ _ ] => setoid_rewrite elem_of_intersection
   | |- context [ _ ∈ _ ∖ _ ] => setoid_rewrite elem_of_difference
-  | |- context [ _ ∈ map _ _ ] => setoid_rewrite elem_of_map
+  | |- context [ _ ∈ _ <$> _ ] => setoid_rewrite elem_of_fmap
+  | |- context [ _ ∈ mret _ ] => setoid_rewrite elem_of_ret
+  | |- context [ _ ∈ _ ≫= _ ] => setoid_rewrite elem_of_bind
+  | |- context [ _ ∈ mjoin _ ] => setoid_rewrite elem_of_join
   end.
 
 (** The tactic [solve_elem_of tac] composes the above tactic with [intuition].
@@ -165,8 +167,8 @@ Tactic Notation "decompose_elem_of" hyp(H) :=
   let rec go H :=
   lazymatch type of H with
   | _ ∈ ∅ => apply elem_of_empty in H; destruct H
-  | ?l ∈ {[ ?l' ]} =>
-    apply elem_of_singleton in H; first [ subst l' | subst l | idtac ]
+  | ?x ∈ {[ ?y ]} =>
+    apply elem_of_singleton in H; try first [subst y | subst x]
   | _ ∈ _ ∪ _ =>
     let H1 := fresh in let H2 := fresh in apply elem_of_union in H;
     destruct H as [H1|H2]; [go H1 | go H2]
@@ -176,9 +178,17 @@ Tactic Notation "decompose_elem_of" hyp(H) :=
   | _ ∈ _ ∖ _ =>
     let H1 := fresh in let H2 := fresh in apply elem_of_difference in H;
     destruct H as [H1 H2]; go H1; go H2
-  | _ ∈ map _ _ =>
-    let H1 := fresh in apply elem_of_map in H;
-    destruct H as [?[? H1]]; go H1
+  | ?x ∈ _ <$> _ =>
+    let H1 := fresh in apply elem_of_fmap in H;
+    destruct H as [? [? H1]]; try (subst x); go H1
+  | _ ∈ _ ≫= _ =>
+    let H1 := fresh in let H2 := fresh in apply elem_of_bind in H;
+    destruct H as [? [H1 H2]]; go H1; go H2
+  | ?x ∈ mret ?y =>
+    apply elem_of_ret in H; try first [subst y | subst x]
+  | _ ∈ mjoin _ ≫= _ =>
+    let H1 := fresh in let H2 := fresh in apply elem_of_join in H;
+    destruct H as [? [H1 H2]]; go H1; go H2
   | _ => idtac
   end in go H.
 Tactic Notation "decompose_elem_of" :=
@@ -186,7 +196,7 @@ Tactic Notation "decompose_elem_of" :=
 
 (** * Sets without duplicates up to an equivalence *)
 Section no_dup.
-  Context `{Collection A B} (R : relation A) `{!Equivalence R}.
+  Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}.
 
   Definition elem_of_upto (x : A) (X : B) := ∃ y, y ∈ X ∧ R x y.
   Definition no_dup (X : B) := ∀ x y, x ∈ X → y ∈ X → R x y → x = y.
@@ -232,7 +242,7 @@ End no_dup.
 
 (** * Quantifiers *)
 Section quantifiers.
-  Context `{Collection A B} (P : A → Prop).
+  Context `{SimpleCollection A B} (P : A → Prop).
 
   Definition cforall X := ∀ x, x ∈ X → P x.
   Definition cexists X := ∃ x, x ∈ X ∧ P x.
@@ -275,7 +285,7 @@ End more_quantifiers.
 (** We collect some properties on the [fresh] operation. In particular we
 generalize [fresh] to generate lists of fresh elements. *)
 Section fresh.
-  Context `{Collection A C} `{Fresh A C} `{!FreshSpec A C} .
+  Context `{FreshSpec A C} .
 
   Definition fresh_sig (X : C) : { x : A | x ∉ X } :=
     exist (∉ X) (fresh X) (is_fresh X).
@@ -300,11 +310,11 @@ Section fresh.
   Lemma fresh_list_length n X : length (fresh_list n X) = n.
   Proof. revert X. induction n; simpl; auto. Qed.
 
-  Lemma fresh_list_is_fresh n X x : In x (fresh_list n X) → x ∉ X.
+  Lemma fresh_list_is_fresh n X x : x ∈ fresh_list n X → x ∉ X.
   Proof.
-    revert X. induction n; simpl.
-    * done.
-    * intros X [?| Hin]. subst.
+    revert X. induction n; intros X; simpl.
+    * by rewrite elem_of_nil.
+    * rewrite elem_of_cons. intros [?| Hin]; subst.
       + apply is_fresh.
       + apply IHn in Hin. solve_elem_of.
   Qed.
@@ -317,3 +327,73 @@ Section fresh.
     solve_elem_of.
   Qed.
 End fresh.
+
+Definition option_collection `{Singleton A C} `{Empty C} (x : option A) : C :=
+  match x with
+  | None => ∅
+  | Some a => {[ a ]}
+  end.
+
+Section collection_monad.
+  Context `{CollectionMonad M}.
+
+  Global Instance collection_guard: MGuard M := λ P dec A x,
+    if dec then x else ∅.
+
+  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.
+  Global Instance collection_bind_proper {A B} (f : A → M B) :
+    Proper ((≡) ==> (≡)) (mbind f).
+  Proof. intros X Y E. esolve_elem_of. Qed.
+  Global Instance collection_join_proper {A} :
+    Proper ((≡) ==> (≡)) (@mjoin M _ A).
+  Proof. intros X Y E. esolve_elem_of. Qed.
+
+  Lemma collection_fmap_compose {A B C} (f : A → B) (g : B → C) X :
+    g ∘ f <$> X ≡ g <$> (f <$> X).
+  Proof. esolve_elem_of. Qed.
+  Lemma elem_of_fmap_1 {A B} (f : A → B) (X : M A) (y : B) :
+    y ∈ f <$> X → ∃ x, y = f x ∧ x ∈ X.
+  Proof. esolve_elem_of. Qed.
+  Lemma elem_of_fmap_2 {A B} (f : A → B) (X : M A) (x : A) :
+    x ∈ X → f x ∈ f <$> X.
+  Proof. esolve_elem_of. Qed.
+  Lemma elem_of_fmap_2_alt {A B} (f : A → B) (X : M A) (x : A) (y : B) :
+    x ∈ X → y = f x → y ∈ f <$> X.
+  Proof. esolve_elem_of. Qed.
+
+  Lemma elem_of_mapM {A B} (f : A → M B) l k :
+    l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k.
+  Proof.
+    split.
+    * revert l. induction k; esolve_elem_of.
+    * induction 1; esolve_elem_of.
+  Qed.
+  Lemma mapM_length {A B} (f : A → M B) l k :
+    l ∈ mapM f k → length l = length k.
+  Proof. revert l; induction k; esolve_elem_of. Qed.
+
+  Lemma elem_of_mapM_fmap {A B} (f : A → B) (g : B → M A) l k :
+    Forall (λ x, ∀ y, y ∈ g x → f y = x) l →
+    k ∈ mapM g l → fmap f k = l.
+  Proof.
+    intros Hl. revert k.
+    induction Hl; simpl; intros;
+      decompose_elem_of; simpl; f_equal; auto.
+  Qed.
+
+  Lemma elem_of_mapM_Forall {A B} (f : A → M B) (P : B → Prop) l k :
+    l ∈ mapM f k →
+    Forall (λ x, ∀ y, y ∈ f x → P y) k →
+    Forall P l.
+  Proof. rewrite elem_of_mapM. apply Forall2_Forall_1. Qed.
+
+  Lemma mapM_non_empty {A B} (f : A → M B) l :
+    Forall (λ x, ∃ y, y ∈ f x) l →
+    ∃ k, k ∈ mapM f l.
+  Proof. induction 1; esolve_elem_of. Qed.
+End collection_monad.
diff --git a/theories/decidable.v b/theories/decidable.v
index e8412ab4..3ed33cb3 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -93,12 +93,14 @@ Instance False_dec: Decision False := right (False_rect False).
 Section prop_dec.
   Context `(P_dec : Decision P) `(Q_dec : Decision Q).
 
+  Global Instance not_dec: Decision (¬P).
+  Proof. refine (cast_if_not P_dec); intuition. Defined.
   Global Instance and_dec: Decision (P ∧ Q).
-  Proof. refine (cast_if_and P_dec Q_dec); intuition. Qed.
+  Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined.
   Global Instance or_dec: Decision (P ∨ Q).
-  Proof. refine (cast_if_or P_dec Q_dec); intuition. Qed.
+  Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined.
   Global Instance impl_dec: Decision (P → Q).
-  Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Qed.
+  Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
 End prop_dec.
 
 (** Instances of [Decision] for common data types. *)
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 3521e255..97814174 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -4,11 +4,11 @@
 importantly, it implements a fold and size function and some useful induction
 principles on finite collections . *)
 Require Import Permutation.
-Require Export collections listset numbers.
+Require Export collections numbers listset.
 
-Instance collection_size `{Elements A C} : Size C := λ X, length (elements X).
-Definition collection_fold `{Elements A C} {B} (f : A → B → B)
-  (b : B) (X : C) : B := foldr f b (elements X).
+Instance collection_size `{Elements A C} : Size C := length ∘ elements.
+Definition collection_fold `{Elements A C} {B}
+  (f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
 
 Section fin_collection.
 Context `{FinCollection A C}.
@@ -23,42 +23,44 @@ Qed.
 Global Instance collection_size_proper: Proper ((≡) ==> (=)) size.
 Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
 
-Lemma size_empty : size ∅ = 0.
+Lemma size_empty : size (∅ : C) = 0.
 Proof.
-  unfold size, collection_size. rewrite (in_nil_inv (elements ∅)).
+  unfold size, collection_size. simpl.
+  rewrite (elem_of_nil_inv (elements ∅)).
   * done.
   * intro. rewrite <-elements_spec. solve_elem_of.
 Qed.
-Lemma size_empty_inv X : size X = 0 → X ≡ ∅.
+Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅.
 Proof.
   intros. apply equiv_empty. intro. rewrite elements_spec.
-  rewrite (nil_length (elements X)); intuition.
+  rewrite (nil_length (elements X)). by rewrite elem_of_nil. done.
 Qed.
-Lemma size_empty_iff X : size X = 0 ↔ X ≡ ∅.
+Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅.
 Proof. split. apply size_empty_inv. intros E. by rewrite E, size_empty. Qed.
 
-Lemma size_singleton x : size {[ x ]} = 1.
+Lemma size_singleton (x : A) : size {[ x ]} = 1.
 Proof.
   change (length (elements {[ x ]}) = length [x]).
   apply Permutation_length, NoDup_Permutation.
   * apply elements_nodup.
   * apply NoDup_singleton.
-  * intros. rewrite <-elements_spec. esolve_elem_of firstorder.
+  * intros.
+    by rewrite <-elements_spec, elem_of_singleton, elem_of_list_singleton.
 Qed.
 Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
 Proof.
-  unfold size, collection_size. rewrite !elements_spec.
+  unfold size, collection_size. simpl. rewrite !elements_spec.
   generalize (elements X). intros [|? l].
   * done.
   * injection 1. intro. rewrite (nil_length l) by done.
-    simpl. intuition congruence.
+    simpl. rewrite !elem_of_list_singleton. congruence.
 Qed.
 
 Lemma elem_of_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
 Proof.
   destruct (elements X) as [|x xs] eqn:E.
   * right. apply equiv_empty. intros x Ex.
-    by rewrite elements_spec, E in Ex.
+    by rewrite elements_spec, E, elem_of_nil in Ex.
   * left. exists x. rewrite elements_spec, E.
     by constructor.
 Qed.
@@ -87,17 +89,17 @@ Qed.
 
 Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y.
 Proof.
-  intros [E _]. unfold size, collection_size. rewrite <-app_length.
+  intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length.
   apply Permutation_length, NoDup_Permutation.
   * apply elements_nodup.
-  * apply NoDup_app; try apply elements_nodup.
+  * apply NoDup_app; repeat split; try apply elements_nodup.
     intros x. rewrite <-!elements_spec. esolve_elem_of.
-  * intros. rewrite in_app_iff, <-!elements_spec. solve_elem_of.
+  * intros. rewrite elem_of_app, <-!elements_spec. solve_elem_of.
 Qed.
 
 Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
 Proof.
-  refine (cast_if (decide_rel In x (elements X)));
+  refine (cast_if (decide_rel (∈) x (elements X)));
     by rewrite (elements_spec _).
 Defined.
 Global Program Instance collection_subseteq_dec_slow (X Y : C) :
@@ -178,11 +180,12 @@ Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B)
   ∀ X, P (collection_fold f b X) X.
 Proof.
   intros ? Hemp Hadd.
-  cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ In x l) → P (foldr f b l) X).
+  cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ x ∈ l) → P (foldr f b l) X).
   { intros help ?. apply help. apply elements_nodup. apply elements_spec. }
-  induction 1 as [|x l ?? IHl]; simpl.
-  * intros X HX. rewrite equiv_empty; firstorder.
-  * intros X HX.
+  induction 1 as [|x l ?? IHl].
+  * intros X HX. setoid_rewrite elem_of_nil in HX.
+    rewrite equiv_empty; firstorder.
+  * intros X HX. setoid_rewrite elem_of_cons in HX.
     rewrite <-(subseteq_union_1 {[ x ]} X) by esolve_elem_of.
     rewrite <-union_difference.
     apply Hadd. solve_elem_of. apply IHl.
@@ -191,25 +194,32 @@ Proof.
     + esolve_elem_of.
 Qed.
 
-Lemma collection_fold_proper {B} (f : A → B → B) (b : B) :
-  (∀ a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) →
-  Proper ((≡) ==> (=)) (collection_fold f b).
-Proof. intros ??? E. apply foldr_permutation. auto. by rewrite E. Qed.
+Lemma collection_fold_proper {B} (R : relation B)
+    `{!Equivalence R}
+    (f : A → B → B) (b : B)
+    `{!Proper ((=) ==> R ==> R) f}
+    (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
+  Proper ((≡) ==> R) (collection_fold f b).
+Proof.
+  intros ?? E. apply (foldr_permutation R f b).
+  * auto.
+  * by rewrite E.
+Qed.
 
 Global Instance cforall_dec `(P : A → Prop)
-    `{∀ x, Decision (P x)} X : Decision (cforall P X) | 100.
+  `{∀ x, Decision (P x)} X : Decision (cforall P X) | 100.
 Proof.
   refine (cast_if (decide (Forall P (elements X))));
-  abstract (unfold cforall; setoid_rewrite elements_spec;
-    by rewrite <-Forall_forall).
+    abstract (unfold cforall; setoid_rewrite elements_spec;
+      by rewrite <-Forall_forall).
 Defined.
 
 Global Instance cexists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X :
   Decision (cexists P X) | 100.
 Proof.
   refine (cast_if (decide (Exists P (elements X))));
-  abstract (unfold cexists; setoid_rewrite elements_spec;
-    by rewrite <-Exists_exists).
+    abstract (unfold cexists; setoid_rewrite elements_spec;
+      by rewrite <-Exists_exists).
 Defined.
 
 Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X :
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a7796501..d767568d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -5,7 +5,6 @@ finite maps and collects some theory on it. Most importantly, it proves useful
 induction principles for finite maps and implements the tactic [simplify_map]
 to simplify goals involving finite maps. *)
 Require Export prelude.
-
 (** * Axiomatization of finite maps *)
 (** We require Leibniz equality to be extensional on finite maps. This of
 course limits the space of finite map implementations, but since we are mainly
@@ -13,14 +12,18 @@ interested in finite maps with numbers as indexes, we do not consider this to
 be a serious limitation. The main application of finite maps is to implement
 the memory, where extensionality of Leibniz equality is very important for a
 convenient use in the assertions of our axiomatic semantics. *)
+
 (** Finiteness is axiomatized by requiring each map to have a finite domain.
 Since we may have multiple implementations of finite sets, the [dom] function is
 parametrized by an implementation of finite sets over the map's key type. *)
+
 (** Finite map implementations are required to implement the [merge] function
 which enables us to give a generic implementation of [union_with],
 [intersection_with], and [difference_with]. *)
-Class FinMap K M `{Lookup K M} `{∀ A, Empty (M A)}
-    `{∀ `(f : A → B), FMap M f} `{PartialAlter K M} `{Dom K M} `{Merge M}
+
+Class FinMap K M `{!FMap M}
+    `{∀ A, Lookup K (M A) A} `{∀ A, Empty (M A)}
+    `{∀ A, PartialAlter K (M A) A} `{∀ A, Dom K (M A)} `{!Merge M}
     `{∀ i j : K, Decision (i = j)} := {
   finmap_eq {A} (m1 m2 : M A) :
     (∀ i, m1 !! i = m2 !! i) → m1 = m2;
@@ -41,19 +44,19 @@ Class FinMap K M `{Lookup K M} `{∀ A, Empty (M A)}
 (** * Derived operations *)
 (** All of the following functions are defined in a generic way for arbitrary
 finite map implementations. These generic implementations do not cause a
-significant enough performance loss to make including them in the finite map
-axiomatization worthwhile. *)
-Instance finmap_alter `{PartialAlter K M} : Alter K M := λ A f,
+significant performance loss to make including them in the finite map interface
+worthwhile. *)
+Instance finmap_insert `{PartialAlter K M A} : Insert K M A := λ i x,
+  partial_alter (λ _, Some x) i.
+Instance finmap_alter `{PartialAlter K M A} : Alter K M A := λ f,
   partial_alter (fmap f).
-Instance finmap_insert `{PartialAlter K M} : Insert K M := λ A k x,
-  partial_alter (λ _, Some x) k.
-Instance finmap_delete `{PartialAlter K M} : Delete K M := λ A,
+Instance finmap_delete `{PartialAlter K M A} : Delete K M :=
   partial_alter (λ _, None).
-Instance finmap_singleton `{PartialAlter K M} {A}
-  `{Empty (M A)} : Singleton (K * A) (M A) := λ p, <[fst p:=snd p]>∅.
 
-Definition list_to_map `{Insert K M} {A} `{Empty (M A)}
-  (l : list (K * A)) : M A := insert_list l ∅.
+Instance finmap_singleton `{PartialAlter K M A}
+  `{Empty M} : Singleton (K * A) M := λ p, <[fst p:=snd p]>∅.
+Definition list_to_map `{Insert K M A} `{Empty M}
+  (l : list (K * A)) : M := insert_list l ∅.
 
 Instance finmap_union_with `{Merge M} : UnionWith M := λ A f,
   merge (union_with f).
@@ -62,408 +65,366 @@ Instance finmap_intersection_with `{Merge M} : IntersectionWith M := λ A f,
 Instance finmap_difference_with `{Merge M} : DifferenceWith M := λ A f,
   merge (difference_with f).
 
-(** Two finite maps are disjoint if they do not have overlapping cells. *)
-Instance finmap_disjoint `{Lookup K M} {A} : Disjoint (M A) := λ m1 m2,
-  ∀ i, m1 !! i = None ∨ m2 !! i = None.
+(** The relation [intersection_forall R] on finite maps describes that the
+relation [R] holds for each pair in the intersection. *)
+Definition intersection_forall `{Lookup K M A} (R : relation A) : relation M :=
+  λ m1 m2, ∀ i x1 x2, m1 !! i = Some x1 → m2 !! i = Some x2 → R x1 x2.
+Instance finmap_disjoint `{∀ A, Lookup K (M A) A} : Disjoint (M A) := λ A,
+  intersection_forall (λ _ _, False).
 
 (** The union of two finite maps only has a meaningful definition for maps
 that are disjoint. However, as working with partial functions is inconvenient
 in Coq, we define the union as a total function. In case both finite maps
 have a value at the same index, we take the value of the first map. *)
-Instance finmap_union `{Merge M} {A} : Union (M A) := union_with (λ x _ , x).
+Instance finmap_union `{Merge M} {A} : Union (M A) :=
+  union_with (λ x _, x).
+Instance finmap_intersection `{Merge M} {A} : Intersection (M A) :=
+  union_with (λ x _, x).
+(** The difference operation removes all values from the first map whose
+index contains a value in the second map as well. *)
+Instance finmap_difference `{Merge M} {A} : Difference (M A) :=
+  difference_with (λ _ _, None).
 
 (** * General theorems *)
-Section finmap.
-Context `{FinMap K M} {A : Type}.
-
-Global Instance finmap_subseteq: SubsetEq (M A) := λ m n,
-  ∀ i x, m !! i = Some x → n !! i = Some x.
-Global Instance: BoundedPreOrder (M A).
-Proof. split; [firstorder |]. intros m i x. by rewrite lookup_empty. Qed.
-
-Lemma lookup_weaken (m1 m2 : M A) i x :
-  m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some x.
-Proof. auto. Qed.
-Lemma lookup_weaken_None (m1 m2 : M A) i :
-  m2 !! i = None → m1 ⊆ m2 → m1 !! i = None.
-Proof. rewrite !eq_None_not_Some. firstorder. Qed.
-Lemma lookup_ne (m : M A) i j : m !! i ≠ m !! j → i ≠ j.
-Proof. congruence. Qed.
-
-Lemma not_elem_of_dom C `{Collection K C} (m : M A) i :
-  i ∉ dom C m ↔ m !! i = None.
-Proof. by rewrite (elem_of_dom C), eq_None_not_Some. Qed.
-
-Lemma finmap_empty (m : M A) : (∀ i, m !! i = None) → m = ∅.
-Proof. intros Hm. apply finmap_eq. intros. by rewrite Hm, lookup_empty. Qed.
-Lemma dom_empty C `{Collection K C} : dom C (∅ : M A) ≡ ∅.
-Proof.
-  split; intro.
-  * rewrite (elem_of_dom C), lookup_empty. by destruct 1.
-  * solve_elem_of.
-Qed.
-Lemma dom_empty_inv C `{Collection K C} (m : M A) : dom C m ≡ ∅ → m = ∅.
-Proof.
-  intros E. apply finmap_empty. intros. apply (not_elem_of_dom C).
-  rewrite E. solve_elem_of.
-Qed.
-
-Lemma lookup_empty_not i : ¬is_Some ((∅ : M A) !! i).
-Proof. rewrite lookup_empty. by destruct 1. Qed.
-Lemma lookup_empty_Some i (x : A) : ¬∅ !! i = Some x.
-Proof. by rewrite lookup_empty. Qed.
-
-Lemma partial_alter_compose (m : M A) i f g :
-  partial_alter (f ∘ g) i m = partial_alter f i (partial_alter g i m).
-Proof.
-  intros. apply finmap_eq. intros ii. case (decide (i = ii)).
-  * intros. subst. by rewrite !lookup_partial_alter.
-  * intros. by rewrite !lookup_partial_alter_ne.
-Qed.
-Lemma partial_alter_comm (m : M A) i j f g :
-  i ≠ j →
- partial_alter f i (partial_alter g j m) = partial_alter g j (partial_alter f i m).
-Proof.
-  intros. apply finmap_eq. intros jj.
-  destruct (decide (jj = j)).
-  * subst. by rewrite lookup_partial_alter_ne,
-     !lookup_partial_alter, lookup_partial_alter_ne.
-  * destruct (decide (jj = i)).
-    + subst. by rewrite lookup_partial_alter,
-       !lookup_partial_alter_ne, lookup_partial_alter by congruence.
-    + by rewrite !lookup_partial_alter_ne by congruence.
-Qed.
-Lemma partial_alter_self_alt (m : M A) i x :
-  x = m !! i → partial_alter (λ _, x) i m = m.
-Proof.
-  intros. apply finmap_eq. intros ii.
-  destruct (decide (i = ii)).
-  * subst. by rewrite lookup_partial_alter.
-  * by rewrite lookup_partial_alter_ne.
-Qed.
-Lemma partial_alter_self (m : M A) i : partial_alter (λ _, m !! i) i m = m.
-Proof. by apply partial_alter_self_alt. Qed.
-
-Lemma lookup_insert (m : M A) i x : <[i:=x]>m !! i = Some x.
-Proof. unfold insert. apply lookup_partial_alter. Qed.
-Lemma lookup_insert_rev (m : M A) i x y : <[i:= x ]>m !! i = Some y → x = y.
-Proof. rewrite lookup_insert. congruence. Qed.
-Lemma lookup_insert_ne (m : M A) i j x : i ≠ j → <[i:=x]>m !! j = m !! j.
-Proof. unfold insert. apply lookup_partial_alter_ne. Qed.
-Lemma insert_comm (m : M A) i j x y :
-  i ≠ j → <[i:=x]>(<[j:=y]>m) = <[j:=y]>(<[i:=x]>m).
-Proof. apply partial_alter_comm. Qed.
-
-Lemma lookup_insert_Some (m : M A) i j x y :
-  <[i:=x]>m !! j = Some y ↔ (i = j ∧ x = y) ∨ (i ≠ j ∧ m !! j = Some y).
-Proof.
-  split.
-  * destruct (decide (i = j)); subst;
-      rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
-  * intros [[??]|[??]].
-    + subst. apply lookup_insert.
-    + by rewrite lookup_insert_ne.
-Qed.
-Lemma lookup_insert_None (m : M A) i j x :
-  <[i:=x]>m !! j = None ↔ m !! j = None ∧ i ≠ j.
-Proof.
-  split.
-  * destruct (decide (i = j)); subst;
-      rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
-  * intros [??]. by rewrite lookup_insert_ne.
-Qed.
-
-Lemma lookup_singleton_Some i j (x y : A) :
-  {[(i, x)]} !! j = Some y ↔ i = j ∧ x = y.
-Proof.
-  unfold singleton, finmap_singleton.
-  rewrite lookup_insert_Some, lookup_empty. simpl.
-  intuition congruence.
-Qed.
-Lemma lookup_singleton_None i j (x : A) :
-  {[(i, x)]} !! j = None ↔ i ≠ j.
-Proof.
-  unfold singleton, finmap_singleton.
-  rewrite lookup_insert_None, lookup_empty. simpl. tauto.
-Qed.
-Lemma insert_singleton i (x y : A) : <[i:=y]>{[(i, x)]} = {[(i, y)]}.
-Proof.
-  unfold singleton, finmap_singleton, insert, finmap_insert.
-  by rewrite <-partial_alter_compose.
-Qed.
-
-Lemma lookup_singleton i (x : A) : {[(i, x)]} !! i = Some x.
-Proof. by rewrite lookup_singleton_Some. Qed.
-Lemma lookup_singleton_ne i j (x : A) : i ≠ j → {[(i, x)]} !! j = None.
-Proof. by rewrite lookup_singleton_None. Qed.
-
-Lemma lookup_delete (m : M A) i : delete i m !! i = None.
-Proof. apply lookup_partial_alter. Qed.
-Lemma lookup_delete_ne (m : M A) i j : i ≠ j → delete i m !! j = m !! j.
-Proof. apply lookup_partial_alter_ne. Qed.
-
-Lemma lookup_delete_Some (m : M A) i j y :
-  delete i m !! j = Some y ↔ i ≠ j ∧ m !! j = Some y.
-Proof.
-  split.
-  * destruct (decide (i = j)); subst;
-      rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence.
-  * intros [??]. by rewrite lookup_delete_ne.
-Qed.
-Lemma lookup_delete_None (m : M A) i j :
-  delete i m !! j = None ↔ i = j ∨ m !! j = None.
-Proof.
-  destruct (decide (i = j)).
-  * subst. rewrite lookup_delete. tauto.
-  * rewrite lookup_delete_ne; tauto.
-Qed.
-
-Lemma delete_empty i : delete i (∅ : M A) = ∅.
-Proof. rewrite <-(partial_alter_self ∅) at 2. by rewrite lookup_empty. Qed.
-Lemma delete_singleton i (x : A) : delete i {[(i, x)]} = ∅.
-Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
-Lemma delete_comm (m : M A) i j : delete i (delete j m) = delete j (delete i m).
-Proof. destruct (decide (i = j)). by subst. by apply partial_alter_comm. Qed.
-Lemma delete_insert_comm (m : M A) i j x :
-  i ≠ j → delete i (<[j:=x]>m) = <[j:=x]>(delete i m).
-Proof. intro. by apply partial_alter_comm. Qed.
-
-Lemma delete_notin (m : M A) i : m !! i = None → delete i m = m.
-Proof.
-  intros. apply finmap_eq. intros j.
-  destruct (decide (i = j)).
-  * subst. by rewrite lookup_delete.
-  * by apply lookup_delete_ne.
-Qed.
-
-Lemma delete_partial_alter (m : M A) i f :
-  m !! i = None → delete i (partial_alter f i m) = m.
-Proof.
-  intros. unfold delete, finmap_delete. rewrite <-partial_alter_compose.
-  rapply partial_alter_self_alt. congruence.
-Qed.
-Lemma delete_partial_alter_dom C `{Collection K C} (m : M A) i f :
-  i ∉ dom C m → delete i (partial_alter f i m) = m.
-Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed.
-Lemma delete_insert (m : M A) i x : m !! i = None → delete i (<[i:=x]>m) = m.
-Proof. apply delete_partial_alter. Qed.
-Lemma delete_insert_dom C `{Collection K C} (m : M A) i x :
-  i ∉ dom C m → delete i (<[i:=x]>m) = m.
-Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed.
-Lemma insert_delete (m : M A) i x : m !! i = Some x → <[i:=x]>(delete i m) = m.
-Proof.
-  intros Hmi. unfold delete, finmap_delete, insert, finmap_insert.
-  rewrite <-partial_alter_compose. unfold compose. rewrite <-Hmi.
-  by apply partial_alter_self_alt.
-Qed.
-
-Lemma elem_of_dom_delete C `{Collection K C} (m : M A) i j :
-  i ∈ dom C (delete j m) ↔ i ≠ j ∧ i ∈ dom C m.
-Proof.
-  rewrite !(elem_of_dom C). unfold is_Some.
-  setoid_rewrite lookup_delete_Some. naive_solver.
-Qed.
-Lemma not_elem_of_dom_delete C `{Collection K C} (m : M A) i :
-  i ∉ dom C (delete i m).
-Proof. apply (not_elem_of_dom C), lookup_delete. Qed.
-
-(** * Induction principles *)
-(** We use the induction principle on finite collections to prove the
-following induction principle on finite maps. *)
-Lemma finmap_ind_alt C (P : M A → Prop) `{FinCollection K C} :
-  P ∅ →
-  (∀ i x m, i ∉ dom C m → P m → P (<[i:=x]>m)) →
-  ∀ m, P m.
-Proof.
-  intros Hemp Hinsert m.
-  apply (collection_ind (λ X, ∀ m, dom C m ≡ X → P m)) with (dom C m).
-  * solve_proper.
-  * clear m. intros m Hm. rewrite finmap_empty.
-    + done.
-    + intros. rewrite <-(not_elem_of_dom C), Hm.
-      by solve_elem_of.
-  * clear m. intros i X Hi IH m Hdom.
-    assert (is_Some (m !! i)) as [x Hx].
-    { apply (elem_of_dom C).
-      rewrite Hdom. clear Hdom.
-      by solve_elem_of. }
-    rewrite <-(insert_delete m i x) by done.
-    apply Hinsert.
-    { by apply (not_elem_of_dom_delete C). }
-    apply IH. apply elem_of_equiv. intros.
-    rewrite (elem_of_dom_delete C).
-    esolve_elem_of.
-  * done.
-Qed.
-
-(** We use the [listset] implementation to prove an induction principle that
-does not mention the map's domain. *)
-Lemma finmap_ind (P : M A → Prop) :
-  P ∅ →
-  (∀ i x m, m !! i = None → P m → P (<[i:=x]>m)) →
-  ∀ m, P m.
-Proof.
-  setoid_rewrite <-(not_elem_of_dom (listset _)).
-  apply (finmap_ind_alt (listset _) P).
-Qed.
-
-(** * Deleting and inserting multiple elements *)
-Lemma lookup_delete_list (m : M A) is j :
-  In j is → delete_list is m !! j = None.
-Proof.
-  induction is as [|i is]; simpl; [done |].
-  intros [?|?].
-  * subst. by rewrite lookup_delete.
-  * destruct (decide (i = j)).
-    + subst. by rewrite lookup_delete.
-    + rewrite lookup_delete_ne; auto.
-Qed.
-Lemma lookup_delete_list_notin (m : M A) is j :
-  ¬In j is → delete_list is m !! j = m !! j.
-Proof.
-  induction is; simpl; [done |].
-  intros. rewrite lookup_delete_ne; tauto.
-Qed.
-
-Lemma delete_list_notin (m : M A) is :
-  Forall (λ i, m !! i = None) is → delete_list is m = m.
-Proof.
-  induction 1; simpl; [done |].
-  rewrite delete_notin; congruence.
-Qed.
-Lemma delete_list_insert_comm (m : M A) is j x :
-  ¬In j is → delete_list is (<[j:=x]>m) = <[j:=x]>(delete_list is m).
-Proof.
-  induction is; simpl; [done |].
-  intros. rewrite IHis, delete_insert_comm; tauto.
-Qed.
-
-Lemma lookup_insert_list (m : M A) l1 l2 i x :
-  (∀y, ¬In (i,y) l1) → insert_list (l1 ++ (i,x) :: l2) m !! i = Some x.
-Proof.
-  induction l1 as [|[j y] l1 IH]; simpl.
-  * intros. by rewrite lookup_insert.
-  * intros Hy. rewrite lookup_insert_ne; naive_solver.
-Qed.
-
-Lemma lookup_insert_list_not_in (m : M A) l i :
-  (∀y, ¬In (i,y) l) → insert_list l m !! i = m !! i.
-Proof.
-  induction l as [|[j y] l IH]; simpl.
-  * done.
-  * intros Hy. rewrite lookup_insert_ne; naive_solver.
-Qed.
-
-(** * Properties of the merge operation *)
-Section merge.
-  Context (f : option A → option A → option A).
-
-  Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f).
-  Proof.
-    intros ??. apply finmap_eq. intros.
-    by rewrite !(merge_spec f), lookup_empty, (left_id None f).
-  Qed.
-  Global Instance: RightId (=) None f → RightId (=) ∅ (merge f).
-  Proof.
-    intros ??. apply finmap_eq. intros.
-    by rewrite !(merge_spec f), lookup_empty, (right_id None f).
-  Qed.
-  Global Instance: Idempotent (=) f → Idempotent (=) (merge f).
-  Proof. intros ??. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed.
-
-  Context `{!PropHolds (f None None = None)}.
-
-  Lemma merge_spec_alt m1 m2 m :
-    (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m.
-  Proof.
-    split; [| intro; subst; apply (merge_spec _) ].
-    intros Hlookup. apply finmap_eq. intros. rewrite Hlookup.
-    apply (merge_spec _).
-  Qed.
-
-  Lemma merge_comm m1 m2 :
-    (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) →
-    merge f m1 m2 = merge f m2 m1.
-  Proof. intros. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed.
-  Global Instance: Commutative (=) f → Commutative (=) (merge f).
-  Proof. intros ???. apply merge_comm. intros. by apply (commutative f). Qed.
-
-  Lemma merge_assoc m1 m2 m3 :
-    (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) =
-          f (f (m1 !! i) (m2 !! i)) (m3 !! i)) →
-    merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
-  Proof. intros. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed.
-  Global Instance: Associative (=) f → Associative (=) (merge f).
-  Proof. intros ????. apply merge_assoc. intros. by apply (associative f). Qed.
-End merge.
-
-(** * Properties of the union and intersection operation *)
-Section union_intersection.
-  Context (f : A → A → A).
-
-  Lemma finmap_union_with_merge m1 m2 i x y :
+Section finmap_common.
+  Context `{FinMap K M} {A : Type}.
+
+  Global Instance finmap_subseteq: SubsetEq (M A) := λ m n,
+    ∀ i x, m !! i = Some x → n !! i = Some x.
+  Global Instance: BoundedPreOrder (M A).
+  Proof. split; [firstorder |]. intros m i x. by rewrite lookup_empty. Qed.
+
+  Lemma lookup_weaken (m1 m2 : M A) i x :
+    m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some x.
+  Proof. auto. Qed.
+  Lemma lookup_weaken_None (m1 m2 : M A) i :
+    m2 !! i = None → m1 ⊆ m2 → m1 !! i = None.
+  Proof.
+    rewrite eq_None_not_Some. intros Hm2 Hm1m2.
+    specialize (Hm1m2 i). destruct (m1 !! i); naive_solver.
+  Qed.
+
+  Lemma lookup_weaken_inv (m1 m2 : M A) i x y :
     m1 !! i = Some x →
+    m1 ⊆ m2 →
     m2 !! i = Some y →
-    union_with f m1 m2 !! i = Some (f x y).
+    x = y.
+  Proof.
+    intros Hm1 ? Hm2. eapply lookup_weaken in Hm1; eauto.
+    congruence.
+  Qed.
+
+  Lemma lookup_ne (m : M A) i j : m !! i ≠ m !! j → i ≠ j.
+  Proof. congruence. Qed.
+
+  Lemma not_elem_of_dom C `{Collection K C} (m : M A) i :
+    i ∉ dom C m ↔ m !! i = None.
+  Proof. by rewrite (elem_of_dom C), eq_None_not_Some. Qed.
+
+  Lemma finmap_empty (m : M A) : (∀ i, m !! i = None) → m = ∅.
+  Proof. intros Hm. apply finmap_eq. intros. by rewrite Hm, lookup_empty. Qed.
+  Lemma dom_empty C `{Collection K C} : dom C (∅ : M A) ≡ ∅.
   Proof.
-    intros Hx Hy. unfold union_with, finmap_union_with.
-    by rewrite (merge_spec _), Hx, Hy.
+    split; intro.
+    * rewrite (elem_of_dom C), lookup_empty. by inversion 1.
+    * solve_elem_of.
   Qed.
-  Lemma finmap_union_with_l m1 m2 i x :
-    m1 !! i = Some x → m2 !! i = None → union_with f m1 m2 !! i = Some x.
+  Lemma dom_empty_inv C `{Collection K C} (m : M A) : dom C m ≡ ∅ → m = ∅.
   Proof.
-    intros Hx Hy. unfold union_with, finmap_union_with.
-    by rewrite (merge_spec _), Hx, Hy.
+    intros E. apply finmap_empty. intros. apply (not_elem_of_dom C).
+    rewrite E. solve_elem_of.
   Qed.
-  Lemma finmap_union_with_r m1 m2 i y :
-    m1 !! i = None → m2 !! i = Some y → union_with f m1 m2 !! i = Some y.
+
+  Lemma lookup_empty_not i : ¬is_Some ((∅ : M A) !! i).
+  Proof. rewrite lookup_empty. by inversion 1. Qed.
+  Lemma lookup_empty_Some i (x : A) : ¬∅ !! i = Some x.
+  Proof. by rewrite lookup_empty. Qed.
+
+  Lemma partial_alter_compose (m : M A) i f g :
+    partial_alter (f ∘ g) i m = partial_alter f i (partial_alter g i m).
   Proof.
-    intros Hx Hy. unfold union_with, finmap_union_with.
-    by rewrite (merge_spec _), Hx, Hy.
+    intros. apply finmap_eq. intros ii. case (decide (i = ii)).
+    * intros. subst. by rewrite !lookup_partial_alter.
+    * intros. by rewrite !lookup_partial_alter_ne.
   Qed.
-  Lemma finmap_union_with_None m1 m2 i :
-    union_with f m1 m2 !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
+  Lemma partial_alter_comm (m : M A) i j f g :
+    i ≠ j →
+      partial_alter f i (partial_alter g j m)
+    = partial_alter g j (partial_alter f i m).
   Proof.
-    unfold union_with, finmap_union_with. rewrite (merge_spec _).
-    destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
+    intros. apply finmap_eq. intros jj.
+    destruct (decide (jj = j)).
+    * subst. by rewrite lookup_partial_alter_ne,
+       !lookup_partial_alter, lookup_partial_alter_ne.
+    * destruct (decide (jj = i)).
+      + subst. by rewrite lookup_partial_alter,
+         !lookup_partial_alter_ne, lookup_partial_alter by congruence.
+      + by rewrite !lookup_partial_alter_ne by congruence.
+  Qed.
+  Lemma partial_alter_self_alt (m : M A) i x :
+    x = m !! i → partial_alter (λ _, x) i m = m.
+  Proof.
+    intros. apply finmap_eq. intros ii.
+    destruct (decide (i = ii)).
+    * subst. by rewrite lookup_partial_alter.
+    * by rewrite lookup_partial_alter_ne.
+  Qed.
+  Lemma partial_alter_self (m : M A) i : partial_alter (λ _, m !! i) i m = m.
+  Proof. by apply partial_alter_self_alt. Qed.
+
+  Lemma lookup_insert (m : M A) i x : <[i:=x]>m !! i = Some x.
+  Proof. unfold insert. apply lookup_partial_alter. Qed.
+  Lemma lookup_insert_rev (m : M A) i x y : <[i:= x ]>m !! i = Some y → x = y.
+  Proof. rewrite lookup_insert. congruence. Qed.
+  Lemma lookup_insert_ne (m : M A) i j x : i ≠ j → <[i:=x]>m !! j = m !! j.
+  Proof. unfold insert. apply lookup_partial_alter_ne. Qed.
+  Lemma insert_comm (m : M A) i j x y :
+    i ≠ j → <[i:=x]>(<[j:=y]>m) = <[j:=y]>(<[i:=x]>m).
+  Proof. apply partial_alter_comm. Qed.
+
+  Lemma lookup_insert_Some (m : M A) i j x y :
+    <[i:=x]>m !! j = Some y ↔ (i = j ∧ x = y) ∨ (i ≠ j ∧ m !! j = Some y).
+  Proof.
+    split.
+    * destruct (decide (i = j)); subst;
+        rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
+    * intros [[??]|[??]].
+      + subst. apply lookup_insert.
+      + by rewrite lookup_insert_ne.
+  Qed.
+  Lemma lookup_insert_None (m : M A) i j x :
+    <[i:=x]>m !! j = None ↔ m !! j = None ∧ i ≠ j.
+  Proof.
+    split.
+    * destruct (decide (i = j)); subst;
+        rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
+    * intros [??]. by rewrite lookup_insert_ne.
+  Qed.
+
+  Lemma lookup_singleton_Some i j (x y : A) :
+    {[(i, x)]} !! j = Some y ↔ i = j ∧ x = y.
+  Proof.
+    unfold singleton, finmap_singleton.
+    rewrite lookup_insert_Some, lookup_empty. simpl.
+    intuition congruence.
+  Qed.
+  Lemma lookup_singleton_None i j (x : A) :
+    {[(i, x)]} !! j = None ↔ i ≠ j.
+  Proof.
+    unfold singleton, finmap_singleton.
+    rewrite lookup_insert_None, lookup_empty. simpl. tauto.
+  Qed.
+  Lemma insert_singleton i (x y : A) : <[i:=y]>{[(i, x)]} = {[(i, y)]}.
+  Proof.
+    unfold singleton, finmap_singleton, insert, finmap_insert.
+    by rewrite <-partial_alter_compose.
+  Qed.
+
+  Lemma lookup_singleton i (x : A) : {[(i, x)]} !! i = Some x.
+  Proof. by rewrite lookup_singleton_Some. Qed.
+  Lemma lookup_singleton_ne i j (x : A) : i ≠ j → {[(i, x)]} !! j = None.
+  Proof. by rewrite lookup_singleton_None. Qed.
+
+  Lemma lookup_delete (m : M A) i : delete i m !! i = None.
+  Proof. apply lookup_partial_alter. Qed.
+  Lemma lookup_delete_ne (m : M A) i j : i ≠ j → delete i m !! j = m !! j.
+  Proof. apply lookup_partial_alter_ne. Qed.
+
+  Lemma lookup_delete_Some (m : M A) i j y :
+    delete i m !! j = Some y ↔ i ≠ j ∧ m !! j = Some y.
+  Proof.
+    split.
+    * destruct (decide (i = j)); subst;
+        rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence.
+    * intros [??]. by rewrite lookup_delete_ne.
+  Qed.
+  Lemma lookup_delete_None (m : M A) i j :
+    delete i m !! j = None ↔ i = j ∨ m !! j = None.
+  Proof.
+    destruct (decide (i = j)).
+    * subst. rewrite lookup_delete. tauto.
+    * rewrite lookup_delete_ne; tauto.
+  Qed.
+
+  Lemma delete_empty i : delete i (∅ : M A) = ∅.
+  Proof. rewrite <-(partial_alter_self ∅) at 2. by rewrite lookup_empty. Qed.
+  Lemma delete_singleton i (x : A) : delete i {[(i, x)]} = ∅.
+  Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
+  Lemma delete_comm (m : M A) i j :
+    delete i (delete j m) = delete j (delete i m).
+  Proof. destruct (decide (i = j)). by subst. by apply partial_alter_comm. Qed.
+  Lemma delete_insert_comm (m : M A) i j x :
+    i ≠ j → delete i (<[j:=x]>m) = <[j:=x]>(delete i m).
+  Proof. intro. by apply partial_alter_comm. Qed.
+
+  Lemma delete_notin (m : M A) i :
+    m !! i = None → delete i m = m.
+  Proof.
+    intros. apply finmap_eq. intros j.
+    destruct (decide (i = j)).
+    * subst. by rewrite lookup_delete.
+    * by apply lookup_delete_ne.
+  Qed.
+
+  Lemma delete_partial_alter (m : M A) i f :
+    m !! i = None → delete i (partial_alter f i m) = m.
+  Proof.
+    intros. unfold delete, finmap_delete. rewrite <-partial_alter_compose.
+    rapply partial_alter_self_alt. congruence.
+  Qed.
+  Lemma delete_partial_alter_dom C `{Collection K C} (m : M A) i f :
+    i ∉ dom C m → delete i (partial_alter f i m) = m.
+  Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed.
+  Lemma delete_insert (m : M A) i x :
+    m !! i = None → delete i (<[i:=x]>m) = m.
+  Proof. apply delete_partial_alter. Qed.
+  Lemma delete_insert_dom C `{Collection K C} (m : M A) i x :
+    i ∉ dom C m → delete i (<[i:=x]>m) = m.
+  Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed.
+  Lemma insert_delete (m : M A) i x :
+    m !! i = Some x → <[i:=x]>(delete i m) = m.
+  Proof.
+    intros Hmi. unfold delete, finmap_delete, insert, finmap_insert.
+    rewrite <-partial_alter_compose. unfold compose. rewrite <-Hmi.
+    by apply partial_alter_self_alt.
+  Qed.
+
+  Lemma elem_of_dom_delete C `{Collection K C} (m : M A) i j :
+    i ∈ dom C (delete j m) ↔ i ≠ j ∧ i ∈ dom C m.
+  Proof.
+    rewrite !(elem_of_dom C), <-!not_eq_None_Some.
+    rewrite lookup_delete_None. intuition.
+  Qed.
+  Lemma not_elem_of_dom_delete C `{Collection K C} (m : M A) i :
+    i ∉ dom C (delete i m).
+  Proof. apply (not_elem_of_dom C), lookup_delete. Qed.
+
+  Lemma lookup_delete_list (m : M A) is j :
+    j ∈ is → delete_list is m !! j = None.
+  Proof.
+    induction 1 as [|i j is]; simpl.
+    * by rewrite lookup_delete.
+    * destruct (decide (i = j)).
+      + subst. by rewrite lookup_delete.
+      + rewrite lookup_delete_ne; auto.
+  Qed.
+  Lemma lookup_delete_list_not_elem_of (m : M A) is j :
+    j ∉ is → delete_list is m !! j = m !! j.
+  Proof.
+    induction is; simpl; [done |].
+    rewrite elem_of_cons. intros.
+    intros. rewrite lookup_delete_ne; intuition.
+  Qed.
+  Lemma delete_list_notin (m : M A) is :
+    Forall (λ i, m !! i = None) is → delete_list is m = m.
+  Proof.
+    induction 1; simpl; [done |].
+    rewrite delete_notin; congruence.
+  Qed.
+
+  Lemma delete_list_insert_comm (m : M A) is j x :
+    j ∉ is → delete_list is (<[j:=x]>m) = <[j:=x]>(delete_list is m).
+  Proof.
+    induction is; simpl; [done |].
+    rewrite elem_of_cons. intros.
+    rewrite IHis, delete_insert_comm; intuition.
+  Qed.
+
+  (** * Induction principles *)
+  (** We use the induction principle on finite collections to prove the
+  following induction principle on finite maps. *)
+  Lemma finmap_ind_alt C (P : M A → Prop) `{FinCollection K C} :
+    P ∅ →
+    (∀ i x m, i ∉ dom C m → P m → P (<[i:=x]>m)) →
+    ∀ m, P m.
+  Proof.
+    intros Hemp Hinsert m.
+    apply (collection_ind (λ X, ∀ m, dom C m ≡ X → P m)) with (dom C m).
+    * solve_proper.
+    * clear m. intros m Hm. rewrite finmap_empty.
+      + done.
+      + intros. rewrite <-(not_elem_of_dom C), Hm.
+        by solve_elem_of.
+    * clear m. intros i X Hi IH m Hdom.
+      assert (∃ x, m !! i = Some x) as [x ?].
+      { apply is_Some_alt, (elem_of_dom C).
+        rewrite Hdom. clear Hdom.
+        by solve_elem_of. }
+      rewrite <-(insert_delete m i x) by done.
+      apply Hinsert.
+      { by apply (not_elem_of_dom_delete C). }
+      apply IH. apply elem_of_equiv. intros.
+      rewrite (elem_of_dom_delete C).
+      esolve_elem_of.
+    * done.
+  Qed.
+
+  (** We use the [listset] implementation to prove an induction principle that
+  does not use the map's domain. *)
+  Lemma finmap_ind (P : M A → Prop) :
+    P ∅ →
+    (∀ i x m, m !! i = None → P m → P (<[i:=x]>m)) →
+    ∀ m, P m.
+  Proof.
+    setoid_rewrite <-(not_elem_of_dom (listset _)).
+    apply (finmap_ind_alt (listset _) P).
   Qed.
 
-  Global Instance: LeftId (=) ∅ (union_with f : M A → M A → M A) := _.
-  Global Instance: RightId (=) ∅ (union_with f : M A → M A → M A) := _.
-  Global Instance:
-    Commutative (=) f → Commutative (=) (union_with f : M A → M A → M A) := _.
-  Global Instance:
-    Associative (=) f → Associative (=) (union_with f : M A → M A → M A) := _.
-  Global Instance:
-    Idempotent (=) f → Idempotent (=) (union_with f : M A → M A → M A) := _.
-End union_intersection.
-
-Lemma finmap_union_Some (m1 m2 : M A) i x :
-  (m1 ∪ m2) !! i = Some x ↔
-    m1 !! i = Some x ∨ (m1 !! i = None ∧ m2 !! i = Some x).
-Proof.
-  unfold union, finmap_union, union_with, finmap_union_with.
-  rewrite (merge_spec _).
-  destruct (m1 !! i), (m2 !! i); compute; try intuition congruence.
-Qed.
-Lemma finmap_union_None (m1 m2 : M A) b :
-  (m1 ∪ m2) !! b = None ↔ m1 !! b = None ∧ m2 !! b = None.
-Proof. apply finmap_union_with_None. Qed.
-End finmap.
+  (** * Properties of the merge operation *)
+  Section merge_with.
+    Context (f : option A → option A → option A).
+
+    Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f).
+    Proof.
+      intros ??. apply finmap_eq. intros.
+      by rewrite !(merge_spec f), lookup_empty, (left_id None f).
+    Qed.
+    Global Instance: RightId (=) None f → RightId (=) ∅ (merge f).
+    Proof.
+      intros ??. apply finmap_eq. intros.
+      by rewrite !(merge_spec f), lookup_empty, (right_id None f).
+    Qed.
+    Global Instance: Idempotent (=) f → Idempotent (=) (merge f).
+    Proof. intros ??. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed.
+
+    Context `{!PropHolds (f None None = None)}.
+
+    Lemma merge_spec_alt m1 m2 m :
+      (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m.
+    Proof.
+      split; [| intro; subst; apply (merge_spec _) ].
+      intros Hlookup. apply finmap_eq. intros. rewrite Hlookup.
+      apply (merge_spec _).
+    Qed.
+
+    Lemma merge_comm m1 m2 :
+      (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) →
+      merge f m1 m2 = merge f m2 m1.
+    Proof. intros. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed.
+    Global Instance: Commutative (=) f → Commutative (=) (merge f).
+    Proof. intros ???. apply merge_comm. intros. by apply (commutative f). Qed.
+
+    Lemma merge_assoc m1 m2 m3 :
+      (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) =
+            f (f (m1 !! i) (m2 !! i)) (m3 !! i)) →
+      merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
+    Proof. intros. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed.
+    Global Instance: Associative (=) f → Associative (=) (merge f).
+    Proof. intros ????. apply merge_assoc. intros. by apply (associative f). Qed.
+  End merge_with.
+End finmap_common.
 
 (** * The finite map tactic *)
 (** The tactic [simplify_map by tac] simplifies finite map expressions
 occuring in the conclusion and hypotheses. It uses [tac] to discharge generated
 inequalities. *)
-Tactic Notation "simplify_map" "by" tactic3(tac) := repeat
+Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
   match goal with
-  | H1 : ?m !! ?i = Some ?x, H2 : ?m !! ?i = Some ?y |- _ =>
-    assert (x = y) by congruence; subst y; clear H2
   | H : context[ ∅ !! _ ] |- _ => rewrite lookup_empty in H
   | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert in H
   | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert_ne in H by tac
-  | H : context[ (delete _ _) !! _ ] |- _ => rewrite lookup_delete in H
-  | H : context[ (delete _ _) !! _ ] |- _ => rewrite lookup_delete_ne in H by tac
+  | H : context[ (delete _ _) !! _] |- _ => rewrite lookup_delete in H
+  | H : context[ (delete _ _) !! _] |- _ => rewrite lookup_delete_ne in H by tac
   | H : context[ {[ _ ]} !! _ ] |- _ => rewrite lookup_singleton in H
   | H : context[ {[ _ ]} !! _ ] |- _ => rewrite lookup_singleton_ne in H by tac
   | |- context[ ∅ !! _ ] => rewrite lookup_empty
@@ -474,8 +435,560 @@ Tactic Notation "simplify_map" "by" tactic3(tac) := repeat
   | |- context[ {[ _ ]} !! _ ] => rewrite lookup_singleton
   | |- context[ {[ _ ]} !! _ ] => rewrite lookup_singleton_ne by tac
   end.
-Tactic Notation "simplify_map" := simplify_map by auto.
+Tactic Notation "simpl_map" := simpl_map by auto.
 
-Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
-  repeat first [ progress (simplify_map by tac) | progress simplify_equality ].
+Tactic Notation "simplify_map_equality" "by" tactic3(tac) := repeat
+  match goal with
+  | _ => progress simpl_map by tac
+  | _ => progress simplify_equality
+  | H1 : ?m1 !! ?i = Some ?x, H2 : ?m2 !! ?i = Some ?y |- _ =>
+    let H3 := fresh in
+    feed pose proof (lookup_weaken_inv m1 m2 i x y) as H3;
+      [done | by tac | done | ];
+    clear H2; symmetry in H3
+  end.
 Tactic Notation "simplify_map_equality" := simplify_map_equality by auto.
+
+Section finmap_more.
+  Context `{FinMap K M} {A : Type}.
+
+  (** * Properties on the relation [intersection_forall] *)
+  Section intersection_forall.
+    Context (R : relation A).
+
+    Global Instance intersection_forall_sym:
+      Symmetric R → Symmetric (intersection_forall R).
+    Proof. firstorder auto. Qed.
+    Lemma intersection_forall_empty_l (m : M A) : intersection_forall R ∅ m.
+    Proof. intros ???. by simpl_map. Qed.
+    Lemma intersection_forall_empty_r (m : M A) : intersection_forall R m ∅.
+    Proof. intros ???. by simpl_map. Qed.
+
+    (** Due to the finiteness of finite maps, we can extract a witness are
+    property does not hold for the intersection. *)
+    Lemma not_intersection_forall `{∀ x y, Decision (R x y)} (m1 m2 : M A) :
+      ¬intersection_forall R m1 m2
+        ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2 ∧ ¬R x1 x2.
+    Proof.
+      split.
+      * intros Hdisjoint.
+        set (Pi i := ∀ x1 x2, m1 !! i = Some x1 → m2 !! i = Some x2 → ¬R x1 x2).
+        assert (∀ i, Decision (Pi i)).
+        { intros i. unfold Decision, Pi.
+          destruct (m1 !! i) as [x1|], (m2 !! i) as [x2|]; try (by left).
+          destruct (decide (R x1 x2)).
+          * naive_solver.
+          * intuition congruence. }
+        destruct (decide (cexists Pi (dom (listset _) m1 ∩ dom (listset _) m2)))
+          as [[i [Hdom Hi]] | Hi].
+        + rewrite elem_of_intersection in Hdom.
+          rewrite !(elem_of_dom (listset _)), !is_Some_alt in Hdom.
+          destruct Hdom as [[x1 ?] [x2 ?]]. exists i x1 x2; auto.
+        + destruct Hdisjoint. intros i x1 x2 Hx1 Hx2.
+          apply dec_stable. intros HP.
+          destruct Hi. exists i.
+          rewrite elem_of_intersection, !(elem_of_dom (listset _)).
+          intuition eauto; congruence.
+      * intros (i & x1 & x2 & Hx1 & Hx2 & Hx1x2) Hdisjoint.
+        by apply Hx1x2, (Hdisjoint i x1 x2).
+    Qed.
+  End intersection_forall.
+
+  (** * Properties on the disjoint maps *)
+  Lemma finmap_disjoint_alt (m1 m2 : M A) :
+    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 finmap_not_disjoint (m1 m2 : M A) :
+    ¬m1 ⊥ m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2.
+  Proof.
+    unfold disjoint, finmap_disjoint.
+    rewrite not_intersection_forall.
+    * firstorder auto.
+    * right. auto.
+  Qed.
+
+  Global Instance: Symmetric (@disjoint (M A) _).
+  Proof. apply intersection_forall_sym. auto. Qed.
+  Lemma finmap_disjoint_empty_l (m : M A) : ∅ ⊥ m.
+  Proof. apply intersection_forall_empty_l. Qed.
+  Lemma finmap_disjoint_empty_r (m : M A) : m ⊥ ∅.
+  Proof. apply intersection_forall_empty_r. Qed.
+
+  Lemma finmap_disjoint_weaken (m1 m1' m2 m2' : M A) :
+    m1' ⊥ m2' →
+    m1 ⊆ m1' → m2 ⊆ m2' →
+    m1 ⊥ m2.
+  Proof.
+    intros Hdisjoint Hm1 Hm2 i x1 x2 Hx1 Hx2.
+    destruct (Hdisjoint i x1 x2); auto.
+  Qed.
+  Lemma finmap_disjoint_weaken_l (m1 m1' m2  : M A) :
+    m1' ⊥ m2 → m1 ⊆ m1' → m1 ⊥ m2.
+  Proof. eauto using finmap_disjoint_weaken. Qed.
+  Lemma finmap_disjoint_weaken_r (m1 m2 m2' : M A) :
+    m1 ⊥ m2' → m2 ⊆ m2' → m1 ⊥ m2.
+  Proof. eauto using finmap_disjoint_weaken. Qed.
+
+  Lemma finmap_disjoint_Some_l (m1 m2 : M A) i x:
+    m1 ⊥ m2 →
+    m1 !! i = Some x →
+    m2 !! i = None.
+  Proof.
+    intros Hdisjoint ?. rewrite eq_None_not_Some, is_Some_alt.
+    intros [x2 ?]. by apply (Hdisjoint i x x2).
+  Qed.
+  Lemma finmap_disjoint_Some_r (m1 m2 : M A) i x:
+    m1 ⊥ m2 →
+    m2 !! i = Some x →
+    m1 !! i = None.
+  Proof. rewrite (symmetry_iff (⊥)). apply finmap_disjoint_Some_l. Qed.
+
+  Lemma finmap_disjoint_singleton_l (m : M A) i x :
+    {[(i, x)]} ⊥ m ↔ m !! i = None.
+  Proof.
+    split.
+    * intro. apply (finmap_disjoint_Some_l {[(i, x)]} _ _ x); by simpl_map.
+    * intros ? j y1 y2 ??.
+      destruct (decide (i = j)); simplify_map_equality; congruence.
+  Qed.
+  Lemma finmap_disjoint_singleton_r (m : M A) i x :
+    m ⊥ {[(i, x)]} ↔ m !! i = None.
+  Proof. by rewrite (symmetry_iff (⊥)), finmap_disjoint_singleton_l. Qed.
+
+  Lemma finmap_disjoint_singleton_l_2 (m : M A) i x :
+    m !! i = None → {[(i, x)]} ⊥ m.
+  Proof. by rewrite finmap_disjoint_singleton_l. Qed.
+  Lemma finmap_disjoint_singleton_r_2 (m : M A) i x :
+    m !! i = None → m ⊥ {[(i, x)]}.
+  Proof. by rewrite finmap_disjoint_singleton_r. Qed.
+
+  (** * Properties of the union and intersection operation *)
+  Section union_intersection_with.
+    Context (f : A → A → A).
+
+    Lemma finmap_union_with_Some m1 m2 i x y :
+      m1 !! i = Some x →
+      m2 !! i = Some y →
+      union_with f m1 m2 !! i = Some (f x y).
+    Proof.
+      intros Hx Hy. unfold union_with, finmap_union_with.
+      by rewrite (merge_spec _), Hx, Hy.
+    Qed.
+    Lemma finmap_union_with_Some_l m1 m2 i x :
+      m1 !! i = Some x →
+      m2 !! i = None →
+      union_with f m1 m2 !! i = Some x.
+    Proof.
+      intros Hx Hy. unfold union_with, finmap_union_with.
+      by rewrite (merge_spec _), Hx, Hy.
+    Qed.
+    Lemma finmap_union_with_Some_r m1 m2 i y :
+      m1 !! i = None →
+      m2 !! i = Some y →
+      union_with f m1 m2 !! i = Some y.
+    Proof.
+      intros Hx Hy. unfold union_with, finmap_union_with.
+      by rewrite (merge_spec _), Hx, Hy.
+    Qed.
+    Lemma finmap_union_with_None m1 m2 i :
+      union_with f m1 m2 !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
+    Proof.
+      unfold union_with, finmap_union_with. rewrite (merge_spec _).
+      destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
+    Qed.
+
+    Global Instance: LeftId (=) ∅ (@union_with M _ _ f).
+    Proof. unfold union_with, finmap_union_with. apply _. Qed.
+    Global Instance: RightId (=) ∅ (@union_with M _ _ f).
+    Proof. unfold union_with, finmap_union_with. apply _. Qed.
+    Global Instance: Commutative (=) f → Commutative (=) (@union_with M _ _ f).
+    Proof. unfold union_with, finmap_union_with. apply _. Qed.
+    Global Instance: Associative (=) f → Associative (=) (@union_with M _ _ f).
+    Proof. unfold union_with, finmap_union_with. apply _. Qed.
+    Global Instance: Idempotent (=) f → Idempotent (=) (@union_with M _ _ f).
+    Proof. unfold union_with, finmap_union_with. apply _. Qed.
+  End union_intersection_with.
+
+  Global Instance: LeftId (=) ∅ (@union (M A) _) := _.
+  Global Instance: RightId (=) ∅ (@union (M A) _) := _.
+  Global Instance: Associative (=) (@union (M A) _) := _.
+  Global Instance: Idempotent (=) (@union (M A) _) := _.
+
+  Lemma finmap_union_Some_raw (m1 m2 : M A) i x :
+    (m1 ∪ m2) !! i = Some x ↔
+      m1 !! i = Some x ∨ (m1 !! i = None ∧ m2 !! i = Some x).
+  Proof.
+    unfold union, finmap_union, union_with, finmap_union_with.
+    rewrite (merge_spec _).
+    destruct (m1 !! i), (m2 !! i); compute; try intuition congruence.
+  Qed.
+  Lemma finmap_union_None (m1 m2 : M A) i :
+    (m1 ∪ m2) !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
+  Proof. apply finmap_union_with_None. Qed.
+
+  Lemma finmap_union_Some (m1 m2 : M A) i x :
+    m1 ⊥ m2 →
+    (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ m2 !! i = Some x.
+  Proof.
+    intros Hdisjoint. rewrite finmap_union_Some_raw.
+    intuition eauto using finmap_disjoint_Some_r.
+  Qed.
+
+  Lemma finmap_union_Some_l (m1 m2 : M A) i x :
+    m1 ⊥ m2 →
+    m1 !! i = Some x →
+    (m1 ∪ m2) !! i = Some x.
+  Proof. intro. rewrite finmap_union_Some; intuition. Qed.
+  Lemma finmap_union_Some_r (m1 m2 : M A) i x :
+    m1 ⊥ m2 →
+    m2 !! i = Some x →
+    (m1 ∪ m2) !! i = Some x.
+  Proof. intro. rewrite finmap_union_Some; intuition. Qed.
+
+  Lemma finmap_union_comm (m1 m2 : M A) :
+    m1 ⊥ m2 →
+    m1 ∪ m2 = m2 ∪ m1.
+  Proof.
+    intros Hdisjoint. apply (merge_comm (union_with (λ x _, x))).
+    intros i. specialize (Hdisjoint i).
+    destruct (m1 !! i), (m2 !! i); compute; naive_solver.
+  Qed.
+
+  Lemma finmap_subseteq_union (m1 m2 : M A) :
+    m1 ⊆ m2 →
+    m1 ∪ m2 = m2.
+  Proof.
+    intros Hm1m2.
+    apply finmap_eq. intros i. apply option_eq. intros x.
+    rewrite finmap_union_Some_raw. split; [by intuition |].
+    intros Hm2. specialize (Hm1m2 i).
+    destruct (m1 !! i) as [y|]; [| by auto].
+    rewrite (Hm1m2 y eq_refl) in Hm2. intuition congruence.
+  Qed.
+  Lemma finmap_subseteq_union_l (m1 m2 : M A) :
+    m1 ⊥ m2 →
+    m1 ⊆ m1 ∪ m2.
+  Proof. intros ? i x. rewrite finmap_union_Some_raw. intuition. Qed.
+  Lemma finmap_subseteq_union_r (m1 m2 : M A) :
+    m1 ⊥ m2 →
+    m2 ⊆ m1 ∪ m2.
+  Proof.
+    intros. rewrite finmap_union_comm by done.
+    by apply finmap_subseteq_union_l.
+  Qed.
+
+  Lemma finmap_disjoint_union_l (m1 m2 m3 : M A) :
+    m1 ∪ m2 ⊥ m3 ↔ m1 ⊥ m3 ∧ m2 ⊥ m3.
+  Proof.
+    rewrite !finmap_disjoint_alt.
+    setoid_rewrite finmap_union_None. naive_solver.
+  Qed.
+  Lemma finmap_disjoint_union_r (m1 m2 m3 : M A) :
+    m1 ⊥ m2 ∪ m3 ↔ m1 ⊥ m2 ∧ m1 ⊥ m3.
+  Proof.
+    rewrite !finmap_disjoint_alt.
+    setoid_rewrite finmap_union_None. naive_solver.
+  Qed.
+  Lemma finmap_disjoint_union_l_2 (m1 m2 m3 : M A) :
+    m1 ⊥ m3 → m2 ⊥ m3 → m1 ∪ m2 ⊥ m3.
+  Proof. by rewrite finmap_disjoint_union_l. Qed.
+  Lemma finmap_disjoint_union_r_2 (m1 m2 m3 : M A) :
+    m1 ⊥ m2 → m1 ⊥ m3 → m1 ⊥ m2 ∪ m3.
+  Proof. by rewrite finmap_disjoint_union_r. Qed.
+  Lemma finmap_union_cancel_l (m1 m2 m3 : M A) :
+    m1 ⊥ m3 →
+    m2 ⊥ m3 →
+    m1 ∪ m3 = m2 ∪ m3 →
+    m1 = m2.
+  Proof.
+    revert m1 m2 m3.
+    cut (∀ (m1 m2 m3 : M A) i x,
+      m1 ⊥ m3 →
+      m2 ⊥ m3 →
+      m1 ∪ m3 = m2 ∪ m3 →
+      m1 !! i = Some x → m2 !! i = Some x).
+    { intros. apply finmap_eq. intros i.
+      apply option_eq. naive_solver. }
+    intros m1 m2 m3 b v Hm1m3 Hm2m3 E ?.
+    destruct (proj1 (finmap_union_Some m2 m3 b v Hm2m3)) as [E2|E2].
+    * rewrite <-E. by apply finmap_union_Some_l.
+    * done.
+    * contradict E2. by apply eq_None_ne_Some, finmap_disjoint_Some_l with m1 v.
+  Qed.
+  Lemma finmap_union_cancel_r (m1 m2 m3 : M A) :
+    m1 ⊥ m3 →
+    m2 ⊥ m3 →
+    m3 ∪ m1 = m3 ∪ m2 →
+    m1 = m2.
+  Proof.
+    intros ??. rewrite !(finmap_union_comm m3) by done.
+    by apply finmap_union_cancel_l.
+  Qed.
+
+  Lemma finmap_union_singleton_l (m : M A) i x :
+    <[i:=x]>m = {[(i,x)]} ∪ m.
+  Proof.
+    apply finmap_eq. intros j. apply option_eq. intros y.
+    rewrite finmap_union_Some_raw.
+    destruct (decide (i = j)); simplify_map_equality; intuition congruence.
+  Qed.
+  Lemma finmap_union_singleton_r (m : M A) i x :
+    m !! i = None →
+    <[i:=x]>m = m ∪ {[(i,x)]}.
+  Proof.
+    intro. rewrite finmap_union_singleton_l, finmap_union_comm; [done |].
+    by apply finmap_disjoint_singleton_l.
+  Qed.
+
+  Lemma finmap_disjoint_insert_l (m1 m2 : M A) i x :
+    <[i:=x]>m1 ⊥ m2 ↔ m2 !! i = None ∧ m1 ⊥ m2.
+  Proof.
+    rewrite finmap_union_singleton_l.
+    by rewrite finmap_disjoint_union_l, finmap_disjoint_singleton_l.
+  Qed.
+  Lemma finmap_disjoint_insert_r (m1 m2 : M A) i x :
+    m1 ⊥ <[i:=x]>m2 ↔ m1 !! i = None ∧ m1 ⊥ m2.
+  Proof.
+    rewrite finmap_union_singleton_l.
+    by rewrite finmap_disjoint_union_r, finmap_disjoint_singleton_r.
+  Qed.
+
+  Lemma finmap_disjoint_insert_l_2 (m1 m2 : M A) i x :
+    m2 !! i = None → m1 ⊥ m2 → <[i:=x]>m1 ⊥ m2.
+  Proof. by rewrite finmap_disjoint_insert_l. Qed.
+  Lemma finmap_disjoint_insert_r_2 (m1 m2 : M A) i x :
+    m1 !! i = None → m1 ⊥ m2 → m1 ⊥ <[i:=x]>m2.
+  Proof. by rewrite finmap_disjoint_insert_r. Qed.
+
+  Lemma finmap_union_insert_l (m1 m2 : M A) i x :
+    <[i:=x]>(m1 ∪ m2) = <[i:=x]>m1 ∪ m2.
+  Proof. by rewrite !finmap_union_singleton_l, (associative (∪)). Qed.
+  Lemma finmap_union_insert_r (m1 m2 : M A) i x :
+    m1 !! i = None →
+    <[i:=x]>(m1 ∪ m2) = m1 ∪ <[i:=x]>m2.
+  Proof.
+    intro. rewrite !finmap_union_singleton_l, !(associative (∪)).
+    rewrite (finmap_union_comm m1); [done |].
+    by apply finmap_disjoint_singleton_r.
+  Qed.
+
+  Lemma finmap_insert_list_union l (m : M A) :
+    insert_list l m = list_to_map l ∪ m.
+  Proof.
+    induction l; simpl.
+    * by rewrite (left_id _ _).
+    * by rewrite IHl, finmap_union_insert_l.
+  Qed.
+
+  Lemma finmap_subseteq_insert (m1 m2 : M A) i x :
+    m1 !! i = None → m1 ⊆ m2 → m1 ⊆ <[i:=x]>m2.
+  Proof.
+    intros ?? j. destruct (decide (j = i)).
+    * intros y ?. congruence.
+    * intros. simpl_map. auto.
+  Qed.
+
+  (** * Properties of the delete operation *)
+  Lemma finmap_disjoint_delete_l (m1 m2 : M A) i :
+    m1 ⊥ m2 → delete i m1 ⊥ m2.
+  Proof.
+    rewrite !finmap_disjoint_alt.
+    intros Hdisjoint j. destruct (Hdisjoint j); auto.
+    rewrite lookup_delete_None. tauto.
+  Qed.
+  Lemma finmap_disjoint_delete_r (m1 m2 : M A) i :
+    m1 ⊥ m2 → m1 ⊥ delete i m2.
+  Proof. symmetry. by apply finmap_disjoint_delete_l. Qed.
+
+  Lemma finmap_disjoint_delete_list_l (m1 m2 : M A) is :
+    m1 ⊥ m2 → delete_list is m1 ⊥ m2.
+  Proof. induction is; simpl; auto using finmap_disjoint_delete_l. Qed.
+  Lemma finmap_disjoint_delete_list_r (m1 m2 : M A) is :
+    m1 ⊥ m2 → m1 ⊥ delete_list is m2.
+  Proof. induction is; simpl; auto using finmap_disjoint_delete_r. Qed.
+
+  Lemma finmap_union_delete (m1 m2 : M A) i :
+    delete i (m1 ∪ m2) = delete i m1 ∪ delete i m2.
+  Proof.
+    intros. apply finmap_eq. intros j. apply option_eq. intros y.
+    destruct (decide (i = j)); simplify_map_equality;
+     rewrite ?finmap_union_Some_raw; simpl_map; intuition congruence.
+  Qed.
+  Lemma finmap_union_delete_list (m1 m2 : M A) is :
+    delete_list is (m1 ∪ m2) = delete_list is m1 ∪ delete_list is m2.
+  Proof.
+    induction is; simpl; [done |].
+    by rewrite IHis, finmap_union_delete.
+  Qed.
+
+  Lemma finmap_disjoint_union_list_l (ms : list (M A)) (m : M A) :
+    ⋃ ms ⊥ m ↔ Forall (⊥ m) ms.
+  Proof.
+    split.
+    * induction ms; simpl; rewrite ?finmap_disjoint_union_l; intuition.
+    * induction 1; simpl.
+      + apply finmap_disjoint_empty_l.
+      + by rewrite finmap_disjoint_union_l.
+  Qed.
+  Lemma finmap_disjoint_union_list_r (ms : list (M A)) (m : M A) :
+    m ⊥ ⋃ ms ↔ Forall (⊥ m) ms.
+  Proof. by rewrite (symmetry_iff (⊥)), finmap_disjoint_union_list_l. Qed.
+
+  Lemma finmap_disjoint_union_list_l_2 (ms : list (M A)) (m : M A) :
+    Forall (⊥ m) ms → ⋃ ms ⊥ m.
+  Proof. by rewrite finmap_disjoint_union_list_l. Qed.
+  Lemma finmap_disjoint_union_list_r_2 (ms : list (M A)) (m : M A) :
+    Forall (⊥ m) ms → m ⊥ ⋃ ms.
+  Proof. by rewrite finmap_disjoint_union_list_r. Qed.
+
+  (** * Properties of the conversion from lists to maps *)
+  Lemma finmap_disjoint_list_to_map_l (m : M A) ixs :
+    list_to_map ixs ⊥ m ↔ Forall (λ ix, m !! fst ix = None) ixs.
+  Proof.
+    split.
+    * induction ixs; simpl; rewrite ?finmap_disjoint_insert_l in *; intuition.
+    * induction 1; simpl.
+      + apply finmap_disjoint_empty_l.
+      + rewrite finmap_disjoint_insert_l. auto.
+  Qed.
+  Lemma finmap_disjoint_list_to_map_r (m : M A) ixs :
+    m ⊥ list_to_map ixs ↔ Forall (λ ix, m !! fst ix = None) ixs.
+  Proof. by rewrite (symmetry_iff (⊥)), finmap_disjoint_list_to_map_l. Qed.
+
+  Lemma finmap_disjoint_list_to_map_zip_l (m : M A) is xs :
+    same_length is xs →
+    list_to_map (zip is xs) ⊥ m ↔ Forall (λ i, m !! i = None) is.
+  Proof.
+    intro. rewrite finmap_disjoint_list_to_map_l.
+    rewrite <-(zip_fst is xs) at 2 by done.
+    by rewrite Forall_fmap.
+  Qed.
+  Lemma finmap_disjoint_list_to_map_zip_r (m : M A) is xs :
+    same_length is xs →
+    m ⊥ list_to_map (zip is xs) ↔ Forall (λ i, m !! i = None) is.
+  Proof.
+    intro. by rewrite (symmetry_iff (⊥)), finmap_disjoint_list_to_map_zip_l.
+  Qed.
+  Lemma finmap_disjoint_list_to_map_zip_l_2 (m : M A) is xs :
+    same_length is xs →
+    Forall (λ i, m !! i = None) is →
+    list_to_map (zip is xs) ⊥ m.
+  Proof. intro. by rewrite finmap_disjoint_list_to_map_zip_l. Qed.
+  Lemma finmap_disjoint_list_to_map_zip_r_2 (m : M A) is xs :
+    same_length is xs →
+    Forall (λ i, m !! i = None) is →
+    m ⊥ list_to_map (zip is xs).
+  Proof. intro. by rewrite finmap_disjoint_list_to_map_zip_r. Qed.
+
+  (** * Properties with respect to vectors of elements *)
+  Lemma finmap_union_delete_vec {n} (ms : vec (M A) n) (i : fin n) :
+    list_disjoint ms →
+    ms !!! i ∪ ⋃ delete (fin_to_nat i) (vec_to_list ms) = ⋃ ms.
+  Proof.
+    induction ms as [|m ? ms]; inversion_clear 1;
+      inv_fin i; simpl; [done | intros i].
+    rewrite (finmap_union_comm m), (associative_eq _ _), IHms.
+    * by apply finmap_union_comm, finmap_disjoint_union_list_l.
+    * done.
+    * by apply finmap_disjoint_union_list_r, Forall_delete.
+  Qed.
+
+  Lemma finmap_union_insert_vec {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 finmap_disjoint_union_r in Hdisjoint.
+    rewrite IH, !(associative_eq (∪)), (finmap_union_comm m); intuition.
+  Qed.
+
+  Lemma finmap_list_disjoint_delete_vec {n} (ms : vec (M A) n) (i : fin n) :
+    list_disjoint ms →
+    Forall (⊥ ms !!! i) (delete (fin_to_nat i) (vec_to_list ms)).
+  Proof.
+    induction ms; inversion_clear 1; inv_fin i; simpl.
+    * done.
+    * constructor. symmetry. by apply Forall_vlookup. auto.
+  Qed.
+
+  Lemma finmap_list_disjoint_insert_vec {n} (ms : vec (M A) n) (i : fin n) m :
+    list_disjoint ms →
+    Forall (⊥ m) (delete (fin_to_nat i) (vec_to_list ms)) →
+    list_disjoint (vinsert i m ms).
+  Proof.
+    induction ms as [|m' ? ms]; inversion_clear 1; inv_fin i; simpl.
+    { constructor; auto. }
+    intros i. inversion_clear 1. constructor; [| by auto].
+    apply Forall_vlookup_2. intros j.
+    destruct (decide (i = j)); subst;
+      rewrite ?vlookup_insert, ?vlookup_insert_ne by done.
+    * done.
+    * by apply Forall_vlookup.
+  Qed.
+
+  (** * Properties of the difference operation *)
+  Lemma finmap_difference_Some (m1 m2 : M A) i x :
+    (m1 ∖ m2) !! i = Some x ↔ m1 !! i = Some x ∧ m2 !! i = None.
+  Proof.
+    unfold difference, finmap_difference, difference_with, finmap_difference_with.
+    rewrite (merge_spec _).
+    destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
+  Qed.
+
+  Lemma finmap_disjoint_difference_l (m1 m2 m3 : M A) :
+    m2 ⊆ m3 → m1 ∖ m3 ⊥ m2.
+  Proof.
+    intros E i. specialize (E i).
+    unfold difference, finmap_difference, difference_with, finmap_difference_with.
+    rewrite (merge_spec _).
+    destruct (m1 !! i), (m2 !! i), (m3 !! i); compute; try intuition congruence.
+    ediscriminate E; eauto.
+  Qed.
+  Lemma finmap_disjoint_difference_r (m1 m2 m3 : M A) :
+    m2 ⊆ m3 → m2 ⊥ m1 ∖ m3.
+  Proof. intros. symmetry. by apply finmap_disjoint_difference_l. Qed.
+
+  Lemma finmap_union_difference (m1 m2 : M A) :
+    m1 ⊆ m2 → m2 = m1 ∪ m2 ∖ m1.
+  Proof.
+    intro Hm1m2. apply finmap_eq. intros i.
+    apply option_eq. intros v. specialize (Hm1m2 i).
+    unfold difference, finmap_difference, difference_with, finmap_difference_with.
+    rewrite finmap_union_Some_raw, (merge_spec _).
+    destruct (m1 !! i) as [v'|], (m2 !! i);
+      try specialize (Hm1m2 v'); compute; intuition congruence.
+  Qed.
+End finmap_more.
+
+(** The tactic [simplify_finmap_disjoint] simplifies occurences of [disjoint]
+in the conclusion and hypotheses that involve the union, insert, or singleton
+operation. *)
+Ltac decompose_finmap_disjoint := repeat
+  match goal with
+  | H : _ ∪ _ ⊥ _ |- _ =>
+    apply finmap_disjoint_union_l in H; destruct H
+  | H : _ ⊥ _ ∪ _ |- _ =>
+    apply finmap_disjoint_union_r in H; destruct H
+  | H : {[ _ ]} ⊥ _ |- _ => apply finmap_disjoint_singleton_l in H
+  | H : _ ⊥ {[ _ ]} |- _ =>  apply finmap_disjoint_singleton_r in H
+  | H : <[_:=_]>_ ⊥ _ |- _ =>
+    apply finmap_disjoint_insert_l in H; destruct H
+  | H : _ ⊥ <[_:=_]>_ |- _ =>
+    apply finmap_disjoint_insert_r in H; destruct H
+  | H : ⋃ _ ⊥ _ |- _ => apply finmap_disjoint_union_list_l in H
+  | H : _ ⊥ ⋃ _ |- _ => apply finmap_disjoint_union_list_r in H
+  | H : ∅ ⊥_ |- _ => clear H
+  | H : _ ⊥ ∅ |- _ => clear H
+  | H : list_disjoint [] |- _ => clear H
+  | H : list_disjoint [_] |- _ => clear H
+  | H : list_disjoint (_ :: _) |- _ =>
+    apply list_disjoint_cons_inv in H; destruct H
+  | H : Forall (⊥ _) _ |- _ => rewrite Forall_vlookup in H
+  | H : Forall (⊥ _) [] |- _ => clear H
+  | H : Forall (⊥ _) (_ :: _) |- _ =>
+    apply Forall_inv in H; destruct H
+  end.
diff --git a/theories/fresh_numbers.v b/theories/fresh_numbers.v
index c75cf774..0be3b557 100644
--- a/theories/fresh_numbers.v
+++ b/theories/fresh_numbers.v
@@ -9,14 +9,14 @@ Definition Nmax `{Elements N C} : C → N := collection_fold Nmax 0%N.
 
 Instance Nmax_proper `{FinCollection N C} : Proper ((≡) ==> (=)) Nmax.
 Proof.
-  apply collection_fold_proper. intros.
-  rewrite !N.max_assoc. f_equal. apply N.max_comm.
+  apply (collection_fold_proper (=)).
+  * solve_proper.
+  * intros. rewrite !N.max_assoc. f_equal. apply N.max_comm.
 Qed.
 
 Lemma Nmax_max `{FinCollection N C} X x : x ∈ X → (x ≤ Nmax X)%N.
 Proof.
-  change ((λ b X, x ∈ X → (x ≤ b)%N) (collection_fold N.max 0%N X) X).
-  apply collection_fold_ind.
+  apply (collection_fold_ind (λ b X, x ∈ X → (x ≤ b)%N)).
   * solve_proper.
   * solve_elem_of.
   * solve_elem_of (eauto using N.le_max_l, N.le_max_r, N.le_trans).
@@ -26,6 +26,7 @@ Instance Nfresh `{FinCollection N C} : Fresh N C := λ l, (1 + Nmax l)%N.
 Instance Nfresh_spec `{FinCollection N C} : FreshSpec N C.
 Proof.
   split.
+  * apply _.
   * intros. unfold fresh, Nfresh.
     setoid_replace X with Y; [done |].
     by apply elem_of_equiv.
diff --git a/theories/list.v b/theories/list.v
index 22ecc074..94de696a 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2,35 +2,22 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects general purpose definitions and theorems on lists that
 are not in the Coq standard library. *)
-Require Import Omega Permutation.
-Require Export base decidable option.
+Require Import Permutation.
+Require Export base decidable option numbers.
 
 Arguments length {_} _.
 Arguments cons {_} _ _.
 Arguments app {_} _ _.
-
-Arguments Forall_nil {_ _}.
-Arguments Forall_cons {_ _} _ _ _ _.
-Arguments Exists_nil {_ _}.
-Arguments Exists_cons {_ _} _ _.
-
-Arguments In {_} _ _.
-Arguments NoDup_nil {_}.
 Arguments Permutation {_} _ _.
+Arguments Forall_cons {_} _ _ _ _ _.
 
 Notation tail := tl.
 Notation take := firstn.
 Notation drop := skipn.
-Notation foldr := fold_right.
-Notation foldl := fold_left.
-
+Notation take_drop := firstn_skipn.
 Arguments take {_} !_ !_ /.
 Arguments drop {_} !_ !_ /.
 
-Notation take_drop := firstn_skipn.
-Notation foldr_app := fold_right_app.
-Notation foldl_app := fold_left_app.
-
 Notation "(::)" := cons (only parsing) : C_scope.
 Notation "( x ::)" := (cons x) (only parsing) : C_scope.
 Notation "(:: l )" := (λ x, cons x l) (only parsing) : C_scope.
@@ -40,46 +27,43 @@ Notation "(++ k )" := (λ l, app l k) (only parsing) : C_scope.
 
 (** * General definitions *)
 (** Looking up elements and updating elements in a list. *)
-Global Instance list_lookup: Lookup nat list :=
-  fix go A (i : nat) (l : list A) {struct l} : option A :=
+Instance list_lookup {A} : Lookup nat (list A) A :=
+  fix go (i : nat) (l : list A) {struct l} : option A :=
   match l with
   | [] => None
   | x :: l =>
     match i with
     | 0 => Some x
-    | S i => @lookup _ _ go _ i l
+    | S i => @lookup _ _ _ go i l
     end
   end.
-
-Global Instance list_alter: Alter nat list :=
-  fix go A (f : A → A) (i : nat) (l : list A) {struct l} :=
+Instance list_alter {A} (f : A → A) : AlterD nat (list A) A f :=
+  fix go (i : nat) (l : list A) {struct l} :=
   match l with
   | [] => []
   | x :: l =>
     match i with
     | 0 => f x :: l
-    | S i => x :: @alter _ _ go _ f i l
+    | S i => x :: @alter _ _ _ f go i l
     end
   end.
-
-Global Instance list_insert: Insert nat list := λ _ i x,
-  alter (λ _, x) i.
-
-Global Instance list_delete: Delete nat list :=
-  fix go A (i : nat) (l : list A) {struct l} : list A :=
+Instance list_delete {A} : Delete nat (list A) :=
+  fix go (i : nat) (l : list A) {struct l} : list A :=
   match l with
   | [] => []
   | x :: l =>
     match i with
     | 0 => l
-    | S i => x :: @delete _ _ go _ i l
+    | S i => x :: @delete _ _ go i l
     end
   end.
+Instance list_insert {A} : Insert nat (list A) A := λ i x,
+  alter (λ _, x) i.
 
 Tactic Notation "discriminate_list_equality" hyp(H) :=
   apply (f_equal length) in H;
   repeat (simpl in H || rewrite app_length in H);
-  exfalso; omega.
+  exfalso; lia.
 Tactic Notation "discriminate_list_equality" :=
   repeat_on_hyps (fun H => discriminate_list_equality H).
 
@@ -91,7 +75,7 @@ Ltac simplify_list_equality := repeat
      | apply app_inv_tail in H ]
   | H : _ |- _ => discriminate_list_equality H
   end.
-    
+
 (** The function [option_list] converts an element of the option type into
 a list. *)
 Definition option_list {A} : option A → list A := option_rect _ (λ x, [x]) [].
@@ -101,56 +85,122 @@ The predicate [suffix_of] holds if the first list is a suffix of the second. *)
 Definition prefix_of {A} (l1 l2 : list A) : Prop := ∃ k, l2 = l1 ++ k.
 Definition suffix_of {A} (l1 l2 : list A) : Prop := ∃ k, l2 = k ++ l1.
 
+(** The function [replicate n x] generates a list with length [n] of elements
+[x]. *)
+Fixpoint replicate {A} (n : nat) (x : A) : list A :=
+  match n with
+  | 0 => []
+  | S n => x :: replicate n x
+  end.
+Definition reverse {A} (l : list A) : list A := rev_append l [].
+
 (** * General theorems *)
 Section general_properties.
 Context {A : Type}.
 
+Global Instance: ∀ k : list A, Injective (=) (=) (k ++).
+Proof. intros ???. apply app_inv_head. Qed.
+Global Instance: ∀ k : list A, Injective (=) (=) (++ k).
+Proof. intros ???. apply app_inv_tail. Qed.
+
 Lemma list_eq (l1 l2 : list A) : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
 Proof.
   revert l2. induction l1; intros [|??] H.
   * done.
   * discriminate (H 0).
   * discriminate (H 0).
-  * f_equal. by injection (H 0). apply IHl1. intro. apply (H (S _)).
+  * f_equal; [by injection (H 0) |].
+    apply IHl1. intro. apply (H (S _)).
 Qed.
+Lemma list_eq_nil (l : list A) : (∀ i, l !! i = None) → l = nil.
+Proof. intros. by apply list_eq. Qed.
 
-Lemma list_lookup_nil i : @nil A !! i = None.
+Global Instance list_eq_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ l k,
+  Decision (l = k) := list_eq_dec dec.
+
+Lemma nil_or_length_pos (l : list A) : l = [] ∨ length l ≠ 0.
+Proof. destruct l; simpl; auto with lia. Qed.
+Lemma nil_length (l : list A) : length l = 0 → l = [].
+Proof. by destruct l. Qed.
+Lemma lookup_nil i : @nil A !! i = None.
 Proof. by destruct i. Qed.
-Lemma list_lookup_tail (l : list A) i : tail l !! i = l !! S i.
+Lemma lookup_tail (l : list A) i : tail l !! i = l !! S i.
 Proof. by destruct l. Qed.
 
-Lemma list_lookup_Some_In (l : list A) i x : l !! i = Some x → In x l.
+Lemma lookup_lt_length (l : list A) i :
+  is_Some (l !! i) ↔ i < length l.
 Proof.
-  revert i. induction l; intros [|i] ?;
-    simpl; simplify_equality; constructor (solve [eauto]).
+  revert i. induction l.
+  * split; by inversion 1.
+  * intros [|?]; simpl.
+    + split; eauto with arith.
+    + by rewrite <-NPeano.Nat.succ_lt_mono.
 Qed.
-
-Lemma list_lookup_In_Some (l : list A) x : In x l → ∃ i, l !! i = Some x.
+Lemma lookup_lt_length_1 (l : list A) i :
+  is_Some (l !! i) → i < length l.
+Proof. apply lookup_lt_length. Qed.
+Lemma lookup_lt_length_alt (l : list A) i x :
+  l !! i = Some x → i < length l.
+Proof. intros Hl. by rewrite <-lookup_lt_length, Hl. Qed.
+Lemma lookup_lt_length_2 (l : list A) i :
+  i < length l → is_Some (l !! i).
+Proof. apply lookup_lt_length. Qed.
+
+Lemma lookup_ge_length (l : list A) i :
+  l !! i = None ↔ length l ≤ i.
+Proof. rewrite eq_None_not_Some, lookup_lt_length. lia. Qed.
+Lemma lookup_ge_length_1 (l : list A) i :
+  l !! i = None → length l ≤ i.
+Proof. by rewrite lookup_ge_length. Qed.
+Lemma lookup_ge_length_2 (l : list A) i :
+  length l ≤ i → l !! i = None.
+Proof. by rewrite lookup_ge_length. Qed.
+
+Lemma lookup_app_l (l1 l2 : list A) i :
+  i < length l1 →
+  (l1 ++ l2) !! i = l1 !! i.
+Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
+Lemma lookup_app_l_Some (l1 l2 : list A) i x :
+  l1 !! i = Some x →
+  (l1 ++ l2) !! i = Some x.
+Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_length_alt. Qed.
+
+Lemma lookup_app_r (l1 l2 : list A) i :
+  (l1 ++ l2) !! (length l1 + i) = l2 !! i.
 Proof.
-  induction l; destruct 1; subst.
-  * by exists 0.
-  * destruct IHl as [i ?]; auto. by exists (S i).
+  revert i.
+  induction l1; intros [|i]; simpl in *; simplify_equality; auto.
+Qed.
+Lemma lookup_app_r_alt (l1 l2 : list A) i :
+  length l1 ≤ i →
+  (l1 ++ l2) !! i = l2 !! (i - length l1).
+Proof.
+  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
+  rewrite Hi at 1. by apply lookup_app_r.
+Qed.
+Lemma lookup_app_r_Some (l1 l2 : list A) i x :
+  l2 !! i = Some x →
+  (l1 ++ l2) !! (length l1 + i) = Some x.
+Proof. by rewrite lookup_app_r. Qed.
+Lemma lookup_app_r_Some_alt (l1 l2 : list A) i x :
+  length l1 ≤ i →
+  l2 !! (i - length l1) = Some x →
+  (l1 ++ l2) !! i = Some x.
+Proof. intro. by rewrite lookup_app_r_alt. Qed.
+
+Lemma lookup_app_inv (l1 l2 : list A) i x :
+  (l1 ++ l2) !! i = Some x →
+  l1 !! i = Some x ∨ l2 !! (i - length l1) = Some x.
+Proof.
+  revert i.
+  induction l1; intros [|i] ?; simpl in *; simplify_equality; auto.
 Qed.
-Lemma list_lookup_In (l : list A) x : In x l ↔ ∃ i, l !! i = Some x.
-Proof. firstorder eauto using list_lookup_Some_In, list_lookup_In_Some. Qed.
 
 Lemma list_lookup_middle (l1 l2 : list A) (x : A) :
   (l1 ++ x :: l2) !! length l1 = Some x.
 Proof. by induction l1; simpl. Qed.
 
-Lemma list_lookup_lt_length (l : list A) i : is_Some (l !! i) ↔ i < length l.
-Proof.
-  revert i. induction l.
-  * split; by inversion 1.
-  * intros [|?]; simpl.
-    + split; auto with arith.
-    + by rewrite <-NPeano.Nat.succ_lt_mono.
-Qed.
-Lemma list_lookup_weaken (l l' : list A) i x :
-  l !! i = Some x → (l ++ l') !! i = Some x.
-Proof. revert i. induction l. done. by intros []. Qed.
-
-Lemma take_lookup i j (l : list A) :
+Lemma lookup_take i j (l : list A) :
   j < i → take i l !! j = l !! j.
 Proof.
   revert i j. induction l; intros [|i] j ?; trivial.
@@ -158,7 +208,7 @@ Proof.
   * destruct j; simpl; auto with arith.
 Qed.
 
-Lemma take_lookup_le i j (l : list A) :
+Lemma lookup_take_le i j (l : list A) :
   i ≤ j → take i l !! j = None.
 Proof.
   revert i j. induction l; intros [|i] [|j] ?; trivial.
@@ -166,25 +216,80 @@ Proof.
   * simpl; auto with arith.
 Qed.
 
-Lemma drop_lookup i j (l : list A) :
+Lemma lookup_drop i j (l : list A) :
   drop i l !! j = l !! (i + j).
 Proof. revert i j. induction l; intros [|i] ?; simpl; auto. Qed.
 
-Lemma list_lookup_alter (f : A → A) i l : alter f i l !! i = f <$> l !! i.
+Lemma alter_length (f : A → A) l i :
+  length (alter f i l) = length l.
+Proof. revert i. induction l; intros [|?]; simpl; auto with lia. Qed.
+Lemma insert_length (l : list A) i x :
+  length (<[i:=x]>l) = length l.
+Proof. apply alter_length. Qed.
+
+Lemma list_lookup_alter (f : A → A) l i :
+  alter f i l !! i = f <$> l !! i.
 Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
-Lemma list_lookup_alter_ne (f : A → A) i j l :
+Lemma list_lookup_alter_ne (f : A → A) l i j :
   i ≠ j → alter f i l !! j = l !! j.
 Proof.
   revert i j. induction l; [done|].
   intros [|i] [|j] ?; try done. apply (IHl i). congruence.
 Qed.
+Lemma list_lookup_insert (l : list A) i x :
+  i < length l →
+  <[i:=x]>l !! i = Some x.
+Proof.
+  intros Hi. unfold insert, list_insert.
+  rewrite list_lookup_alter.
+  by feed inversion (lookup_lt_length_2 l i).
+Qed.
+Lemma list_lookup_insert_ne (l : list A) i j x :
+  i ≠ j → <[i:=x]>l !! j = l !! j.
+Proof. apply list_lookup_alter_ne. Qed.
+
+Lemma alter_app_l (f : A → A) (l1 l2 : list A) i :
+  i < length l1 →
+  alter f i (l1 ++ l2) = alter f i l1 ++ l2.
+Proof.
+  revert i.
+  induction l1; intros [|?] ?; simpl in *; f_equal; auto with lia.
+Qed.
+Lemma alter_app_r (f : A → A) (l1 l2 : list A) i :
+  alter f (length l1 + i) (l1 ++ l2) = l1 ++ alter f i l2.
+Proof.
+  revert i.
+  induction l1; intros [|?]; simpl in *; f_equal; auto.
+Qed.
+Lemma alter_app_r_alt (f : A → A) (l1 l2 : list A) i :
+  length l1 ≤ i →
+  alter f i (l1 ++ l2) = l1 ++ alter f (i - length l1) l2.
+Proof.
+  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
+  rewrite Hi at 1. by apply alter_app_r.
+Qed.
 
+Lemma insert_app_l (l1 l2 : list A) i x :
+  i < length l1 →
+  <[i:=x]>(l1 ++ l2) = <[i:=x]>l1 ++ l2.
+Proof. apply alter_app_l. Qed.
+Lemma insert_app_r (l1 l2 : list A) i x :
+  <[length l1 + i:=x]>(l1 ++ l2) = l1 ++ <[i:=x]>l2.
+Proof. apply alter_app_r. Qed.
+Lemma insert_app_r_alt (l1 l2 : list A) i x :
+  length l1 ≤ i →
+  <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2.
+Proof. apply alter_app_r_alt. Qed.
+
+Lemma take_nil i :
+  take i (@nil A) = [].
+Proof. by destruct i. Qed.
 Lemma take_alter (f : A → A) i j l :
   i ≤ j → take i (alter f j l) = take i l.
 Proof.
   intros. apply list_eq. intros jj. destruct (le_lt_dec i jj).
-  * by rewrite !take_lookup_le.
-  * by rewrite !take_lookup, !list_lookup_alter_ne by omega.
+  * by rewrite !lookup_take_le.
+  * by rewrite !lookup_take, !list_lookup_alter_ne by lia.
 Qed.
 Lemma take_insert i j (x : A) l :
   i ≤ j → take i (<[j:=x]>l) = take i l.
@@ -194,299 +299,520 @@ Lemma drop_alter (f : A → A) i j l :
   j < i → drop i (alter f j l) = drop i l.
 Proof.
   intros. apply list_eq. intros jj.
-  by rewrite !drop_lookup, !list_lookup_alter_ne by omega.
+  by rewrite !lookup_drop, !list_lookup_alter_ne by lia.
 Qed.
 Lemma drop_insert i j (x : A) l :
   j < i → drop i (<[j:=x]>l) = drop i l.
 Proof drop_alter _ _ _ _.
 
-Lemma foldr_permutation {B} (f : A → B → B) (b : B) :
-  (∀ a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) →
-  Proper (Permutation ==> (=)) (foldr f b).
-Proof. intro. induction 1; simpl; congruence. Qed.
+Lemma insert_consecutive_length (l : list A) i k :
+  length (insert_consecutive i k l) = length l.
+Proof. revert i. by induction k; intros; simpl; rewrite ?insert_length. Qed.
 
-Lemma Forall_cons_inv (P : A → Prop) x l :
-  Forall P (x :: l) → P x ∧ Forall P l.
-Proof. by inversion_clear 1. Qed.
-
-Lemma Forall_app (P : A → Prop) l1 l2 :
-  Forall P (l1 ++ l2) ↔ Forall P l1 ∧ Forall P l2.
+Lemma not_elem_of_nil (x : A) : x ∉ [].
+Proof. by inversion 1. Qed.
+Lemma elem_of_nil (x : A) : x ∈ [] ↔ False.
+Proof. intuition. by destruct (not_elem_of_nil x). Qed.
+Lemma elem_of_nil_inv (l : list A) : (∀ x, x ∉ l) → l = [].
+Proof. destruct l. done. by edestruct 1; constructor. Qed.
+Lemma elem_of_cons (x y : A) l :
+  x ∈ y :: l ↔ x = y ∨ x ∈ l.
 Proof.
   split.
-   induction l1; inversion 1; intuition.
-  intros [H ?]. induction H; simpl; intuition.
+  * inversion 1; subst. by left. by right.
+  * intros [?|?]; subst. by left. by right.
 Qed.
-
-Lemma Forall_true (P : A → Prop) l :
-  (∀ x, P x) → Forall P l.
-Proof. induction l; auto. Qed.
-Lemma Forall_impl (P Q : A → Prop) l :
-  Forall P l → (∀ x, P x → Q x) → Forall Q l.
-Proof. induction 1; auto. Qed.
-Lemma Forall_delete (P : A → Prop) l i :
-  Forall P l → Forall P (delete i l).
+Lemma elem_of_app (x : A) l1 l2 :
+  x ∈ l1 ++ l2 ↔ x ∈ l1 ∨ x ∈ l2.
 Proof.
-  intros H. revert i.
-  by induction H; intros [|i]; try constructor.
+  induction l1.
+  * split; [by right|]. intros [Hx|]; [|done].
+    by destruct (elem_of_nil x).
+  * simpl. rewrite !elem_of_cons, IHl1. tauto.
 Qed.
+Lemma elem_of_list_singleton (x y : A) : x ∈ [y] ↔ x = y.
+Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.
 
-Lemma Forall2_length {B} (P : A → B → Prop) l1 l2 :
-  Forall2 P l1 l2 → length l1 = length l2.
-Proof. induction 1; simpl; auto. Qed.
+Global Instance elem_of_list_permutation_proper (x : A) :
+  Proper (Permutation ==> iff) (x ∈).
+Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
 
-Lemma Forall2_impl {B} (P Q : A → B → Prop) l1 l2 :
-  Forall2 P l1 l2 → (∀ x y, P x y → Q x y) → Forall2 Q l1 l2.
-Proof. induction 1; auto. Qed.
+Lemma elem_of_list_split (x : A) l :
+  x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2.
+Proof.
+  induction 1 as [x l|x y l ? [l1 [l2 ?]]].
+  * by eexists [], l.
+  * subst. by exists (y :: l1) l2.
+Qed.
 
-Lemma Forall2_unique {B} (P : A → B → Prop) l k1 k2 :
-  Forall2 P l k1 →
-  Forall2 P l k2 →
-  (∀ x y1 y2, P x y1 → P x y2 → y1 = y2) →
-  k1 = k2.
+Global Instance elem_of_list_dec {dec : ∀ x y : A, Decision (x = y)} :
+  ∀ (x : A) l, Decision (x ∈ l).
+Proof.
+ intros x. refine (
+  fix go l :=
+  match l return Decision (x ∈ l) with
+  | [] => right (not_elem_of_nil _)
+  | y :: l => cast_if_or (decide_rel (=) x y) (go l)
+  end); clear go dec; subst; try (by constructor); by inversion 1.
+Defined.
+
+Lemma elem_of_list_lookup_1 (l : list A) x :
+  x ∈ l → ∃ i, l !! i = Some x.
+Proof.
+  induction 1 as [|???? IH].
+  * by exists 0.
+  * destruct IH as [i ?]; auto. by exists (S i).
+Qed.
+Lemma elem_of_list_lookup_2 (l : list A) i x :
+  l !! i = Some x → x ∈ l.
+Proof.
+  revert i. induction l; intros [|i] ?;
+    simpl; simplify_equality; constructor; eauto.
+Qed.
+Lemma elem_of_list_lookup (l : list A) x :
+  x ∈ l ↔ ∃ i, l !! i = Some x.
 Proof.
-  intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto.
+  firstorder eauto using
+    elem_of_list_lookup_1, elem_of_list_lookup_2.
 Qed.
 
+Lemma NoDup_nil : NoDup (@nil A) ↔ True.
+Proof. split; constructor. Qed.
+Lemma NoDup_cons (x : A) l : NoDup (x :: l) ↔ x ∉ l ∧ NoDup l.
+Proof. split. by inversion 1. intros [??]. by constructor. Qed.
+Lemma NoDup_cons_11 (x : A) l : NoDup (x :: l) → x ∉ l.
+Proof. rewrite NoDup_cons. by intros [??]. Qed.
+Lemma NoDup_cons_12 (x : A) l : NoDup (x :: l) → NoDup l.
+Proof. rewrite NoDup_cons. by intros [??]. Qed.
 Lemma NoDup_singleton (x : A) : NoDup [x].
-Proof. constructor. intros []. constructor. Qed.
+Proof. constructor. apply not_elem_of_nil. constructor. Qed.
+
 Lemma NoDup_app (l k : list A) :
-  NoDup l → NoDup k → (∀ x, In x l → ¬In x k) → NoDup (l ++ k).
+  NoDup (l ++ k) ↔ NoDup l ∧ (∀ x, x ∈ l → x ∉ k) ∧ NoDup k.
 Proof.
-  induction 1; simpl.
-  * done.
-  * constructor; rewrite ?in_app_iff; firstorder.
+  induction l; simpl.
+  * rewrite NoDup_nil.
+    setoid_rewrite elem_of_nil. naive_solver.
+  * rewrite !NoDup_cons.
+    setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app.
+    naive_solver.
 Qed.
 
-Global Instance: ∀ k : list A, Injective (=) (=) (k ++).
-Proof. intros ???. apply app_inv_head. Qed.
-Global Instance: ∀ k : list A, Injective (=) (=) (++ k).
-Proof. intros ???. apply app_inv_tail. Qed.
-
-Lemma in_nil_inv (l : list A) : (∀ x, ¬In x l) → l = [].
-Proof. destruct l. done. by edestruct 1; constructor. Qed.
-Lemma nil_length (l : list A) : length l = 0 → l = [].
-Proof. by destruct l. Qed.
-Lemma NoDup_inv_1 (x : A) (l : list A) : NoDup (x :: l) → ¬In x l.
-Proof. by inversion_clear 1. Qed.
-Lemma NoDup_inv_2 (x : A) (l : list A) : NoDup (x :: l) → NoDup l.
-Proof. by inversion_clear 1. Qed.
-Lemma Forall_inv_2 (P : A → Prop) x l : Forall P (x :: l) → Forall P l.
-Proof. by inversion 1. Qed.
-Lemma Exists_inv (P : A → Prop) x l : Exists P (x :: l) → P x ∨ Exists P l.
-Proof. inversion 1; intuition trivial. Qed.
-
-Definition reverse (l : list A) : list A := rev_append l [].
-
-Lemma reverse_nill : reverse [] = [].
-Proof. done. Qed.
-Lemma reverse_cons x l : reverse (x :: l) = reverse l ++ [x].
-Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
-Lemma reverse_snoc x l : reverse (l ++ [x]) = x :: reverse l.
-Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
-Lemma reverse_app l1 l2 : reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
-Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
-Lemma reverse_length l : length (reverse l) = length l.
-Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
-Lemma reverse_involutive l : reverse (reverse l) = l.
-Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed. 
+Global Instance NoDup_permutation_proper:
+  Proper (Permutation ==> iff) (@NoDup A).
+Proof.
+  induction 1 as [|x l k Hlk IH | |].
+  * by rewrite !NoDup_nil.
+  * by rewrite !NoDup_cons, IH, Hlk.
+  * rewrite !NoDup_cons, !elem_of_cons. intuition.
+  * intuition.
+Qed.
 
-Global Instance list_eq_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ l k,
-  Decision (l = k) := list_eq_dec dec.
-Global Instance In_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ x l,
-  Decision (In x l) := in_dec dec.
+Lemma NoDup_Permutation (l k : list A) :
+  NoDup l → NoDup k → (∀ x, x ∈ l ↔ x ∈ k) → Permutation l k.
+Proof.
+  intros Hl. revert k. induction Hl as [|x l Hin ? IH].
+  * intros k _ Hk.
+    rewrite (elem_of_nil_inv k); [done |].
+    intros x. rewrite <-Hk, elem_of_nil. intros [].
+  * intros k Hk Hlk.
+    destruct (elem_of_list_split x k) as [l1 [l2 ?]]; subst.
+    { rewrite <-Hlk. by constructor. }
+    rewrite <-Permutation_middle, NoDup_cons in Hk.
+    destruct Hk as [??].
+    apply Permutation_cons_app, IH; [done |].
+    intros y. specialize (Hlk y).
+    rewrite <-Permutation_middle, !elem_of_cons in Hlk.
+    naive_solver.
+Qed.
 
 Global Instance NoDup_dec {dec : ∀ x y : A, Decision (x = y)} :
     ∀ (l : list A), Decision (NoDup l) :=
   fix NoDup_dec l :=
   match l return Decision (NoDup l) with
-  | [] => left NoDup_nil
+  | [] => left NoDup_nil_2
   | x :: l =>
-    match In_dec x l with
-    | left Hin => right (λ H, NoDup_inv_1 _ _ H Hin)
+    match decide_rel (∈) x l with
+    | left Hin => right (λ H, NoDup_cons_11 _ _ H Hin)
     | right Hin =>
       match NoDup_dec l with
-      | left H => left (NoDup_cons _ Hin H)
-      | right H => right (H ∘ NoDup_inv_2 _ _)
+      | left H => left (NoDup_cons_2 _ _ Hin H)
+      | right H => right (H ∘ NoDup_cons_12 _ _)
       end
     end
   end.
 
-Section Forall_Exists.
-Context (P : A → Prop).
+Section remove_dups.
+  Context `{!∀ x y : A, Decision (x = y)}.
 
-Lemma Exists_not_Forall l : Exists (not ∘ P) l → ¬Forall P l.
-Proof. induction 1; inversion_clear 1; contradiction. Qed.
+  Fixpoint remove_dups (l : list A) : list A :=
+    match l with
+    | [] => []
+    | x :: l =>
+      if decide_rel (∈) x l then remove_dups l else x :: remove_dups l
+    end.
 
-Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l.
-Proof. induction 1; inversion_clear 1; contradiction. Qed.
+  Lemma elem_of_remove_dups l x :
+    x ∈ remove_dups l ↔ x ∈ l.
+  Proof.
+    split; induction l; simpl; repeat case_decide;
+      rewrite ?elem_of_cons; intuition (simplify_equality; auto).
+  Qed.
 
-Context {dec : ∀ x, Decision (P x)}.
+  Lemma remove_dups_nodup l : NoDup (remove_dups l).
+  Proof.
+    induction l; simpl; repeat case_decide; try constructor; auto.
+    by rewrite elem_of_remove_dups.
+  Qed.
+End remove_dups.
 
-Fixpoint Forall_Exists_dec l : {Forall P l} + {Exists (not ∘ P) l}.
+Lemma reverse_nil : reverse [] = @nil A.
+Proof. done. Qed.
+Lemma reverse_cons (l : list A) x : reverse (x :: l) = reverse l ++ [x].
+Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
+Lemma reverse_snoc (l : list A) x : reverse (l ++ [x]) = x :: reverse l.
+Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
+Lemma reverse_app (l1 l2 : list A) :
+  reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
+Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
+Lemma reverse_length (l : list A) : length (reverse l) = length l.
+Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
+Lemma reverse_involutive (l : list A) : reverse (reverse l) = l.
+Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed. 
+
+Lemma replicate_length n (x : A) : length (replicate n x) = n.
+Proof. induction n; simpl; auto. Qed.
+Lemma lookup_replicate n (x : A) i :
+  i < n →
+  replicate n x !! i = Some x.
 Proof.
- refine (
-  match l with
-  | [] => left _
-  | x :: l => cast_if_and (dec x) (Forall_Exists_dec l)
-  end); clear Forall_Exists_dec; abstract intuition.
-Defined.
+  revert i.
+  induction n; intros [|?]; naive_solver auto with lia.
+Qed.
+Lemma lookup_replicate_inv n (x y : A) i :
+  replicate n x !! i = Some y → y = x ∧ i < n.
+Proof.
+  revert i.
+  induction n; intros [|?]; naive_solver auto with lia.
+Qed.
 
-Lemma not_Forall_Exists l : ¬Forall P l → Exists (not ∘ P) l.
-Proof. intro. destruct (Forall_Exists_dec l); intuition. Qed.
+Section Forall_Exists.
+  Context (P : A → Prop).
 
-Global Instance Forall_dec l : Decision (Forall P l) :=
-  match Forall_Exists_dec l with
-  | left H => left H
-  | right H => right (Exists_not_Forall _ H)
-  end.
+  Lemma Forall_forall l :
+    Forall P l ↔ ∀ x, x ∈ l → P x.
+  Proof.
+    split.
+    * induction 1; inversion 1; subst; auto.
+    * intros Hin. induction l; constructor.
+      + apply Hin. constructor.
+      + apply IHl. intros ??. apply Hin. by constructor.
+  Qed.
+  Lemma Forall_inv x l : Forall P (x :: l) → P x ∧ Forall P l.
+  Proof. by inversion 1. Qed.
+  Lemma Forall_inv_1 x l : Forall P (x :: l) → P x.
+  Proof. by inversion 1. Qed.
+  Lemma Forall_inv_2 x l : Forall P (x :: l) → Forall P l.
+  Proof. by inversion 1. Qed.
+
+  Lemma Forall_app l1 l2 : Forall P (l1 ++ l2) ↔ Forall P l1 ∧ Forall P l2.
+  Proof.
+    split.
+    * induction l1; inversion 1; intuition.
+    * intros [H ?]. induction H; simpl; intuition.
+  Qed.
+  Lemma Forall_true l : (∀ x, P x) → Forall P l.
+  Proof. induction l; auto. Qed.
+  Lemma Forall_impl l (Q : A → Prop) :
+    Forall P l → (∀ x, P x → Q x) → Forall Q l.
+  Proof. intros H ?. induction H; auto. Defined.
+  Lemma Forall_delete l i : Forall P l → Forall P (delete i l).
+  Proof.
+    intros H. revert i.
+    by induction H; intros [|i]; try constructor.
+  Qed.
+  Lemma Forall_lookup l :
+    Forall P l ↔ ∀ i x, l !! i = Some x → P x.
+  Proof.
+    rewrite Forall_forall.
+    setoid_rewrite elem_of_list_lookup.
+    naive_solver.
+  Qed.
+  Lemma Forall_alter f l i :
+    Forall P l →
+    (∀ x, l !! i = Some x → P x → P (f x)) →
+    Forall P (alter f i l).
+  Proof.
+    intros Hl. revert i.
+    induction Hl; simpl; intros [|i]; constructor; auto.
+  Qed.
 
-Fixpoint Exists_Forall_dec l : {Exists P l} + {Forall (not ∘ P) l}.
-Proof.
- refine (
-  match l with
-  | [] => right _
-  | x :: l => cast_if_or (dec x) (Exists_Forall_dec l)
-  end); clear Exists_Forall_dec; abstract intuition.
-Defined.
+  Lemma Exists_exists l :
+    Exists P l ↔ ∃ x, x ∈ l ∧ P x.
+  Proof.
+    split.
+    * induction 1 as [x|y ?? IH].
+      + exists x. split. constructor. done.
+      + destruct IH as [x [??]]. exists x. split. by constructor. done. 
+    * intros [x [Hin ?]]. induction l.
+      + by destruct (not_elem_of_nil x).
+      + inversion Hin; subst. by left. right; auto.
+  Qed.
+  Lemma Exists_inv x l : Exists P (x :: l) → P x ∨ Exists P l.
+  Proof. inversion 1; intuition trivial. Qed.
+  Lemma Exists_app l1 l2 : Exists P (l1 ++ l2) ↔ Exists P l1 ∨ Exists P l2.
+  Proof.
+    split.
+    * induction l1; inversion 1; intuition.
+    * intros [H|H].
+      + induction H; simpl; intuition.
+      + induction l1; simpl; intuition. 
+  Qed.
 
-Lemma not_Exists_Forall l : ¬Exists P l → Forall (not ∘ P) l.
-Proof. intro. destruct (Exists_Forall_dec l); intuition. Qed.
+  Lemma Exists_not_Forall l : Exists (not ∘ P) l → ¬Forall P l.
+  Proof. induction 1; inversion_clear 1; contradiction. Qed.
+  Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l.
+  Proof. induction 1; inversion_clear 1; contradiction. Qed.
 
-Global Instance Exists_dec l : Decision (Exists P l) :=
-  match Exists_Forall_dec l with
-  | left H => left H
-  | right H => right (Forall_not_Exists _ H)
-  end.
+  Context {dec : ∀ x, Decision (P x)}.
+
+  Fixpoint Forall_Exists_dec l : {Forall P l} + {Exists (not ∘ P) l}.
+  Proof.
+   refine (
+    match l with
+    | [] => left _
+    | x :: l => cast_if_and (dec x) (Forall_Exists_dec l)
+    end); clear Forall_Exists_dec; abstract intuition.
+  Defined.
+
+  Lemma not_Forall_Exists l : ¬Forall P l → Exists (not ∘ P) l.
+  Proof. intro. destruct (Forall_Exists_dec l); intuition. Qed.
+
+  Global Instance Forall_dec l : Decision (Forall P l) :=
+    match Forall_Exists_dec l with
+    | left H => left H
+    | right H => right (Exists_not_Forall _ H)
+    end.
+
+  Fixpoint Exists_Forall_dec l : {Exists P l} + {Forall (not ∘ P) l}.
+  Proof.
+   refine (
+    match l with
+    | [] => right _
+    | x :: l => cast_if_or (dec x) (Exists_Forall_dec l)
+    end); clear Exists_Forall_dec; abstract intuition.
+  Defined.
+
+  Lemma not_Exists_Forall l : ¬Exists P l → Forall (not ∘ P) l.
+  Proof. intro. destruct (Exists_Forall_dec l); intuition. Qed.
+
+  Global Instance Exists_dec l : Decision (Exists P l) :=
+    match Exists_Forall_dec l with
+    | left H => left H
+    | right H => right (Forall_not_Exists _ H)
+    end.
 End Forall_Exists.
+
+Section Forall2.
+  Context {B} (P : A → B → Prop).
+
+  Lemma Forall2_length l1 l2 :
+    Forall2 P l1 l2 → length l1 = length l2.
+  Proof. induction 1; simpl; auto. Qed.
+  Lemma Forall2_impl (Q : A → B → Prop) l1 l2 :
+    Forall2 P l1 l2 → (∀ x y, P x y → Q x y) → Forall2 Q l1 l2.
+  Proof. induction 1; auto. Qed.
+
+  Lemma Forall2_unique l k1 k2 :
+    Forall2 P l k1 →
+    Forall2 P l k2 →
+    (∀ x y1 y2, P x y1 → P x y2 → y1 = y2) →
+    k1 = k2.
+  Proof.
+    intros H. revert k2.
+    induction H; inversion_clear 1; intros; f_equal; eauto.
+  Qed.
+
+  Lemma Forall2_Forall_1 (Q : A → Prop) l k :
+    Forall2 P l k →
+    Forall (λ y, ∀ x, P x y → Q x) k →
+    Forall Q l.
+  Proof. induction 1; inversion_clear 1; constructor; eauto. Qed.
+  Lemma Forall2_Forall_2 (Q : B → Prop) l k :
+    Forall2 P l k →
+    Forall (λ x, ∀ y, P x y → Q y) l →
+    Forall Q k.
+  Proof. induction 1; inversion_clear 1; constructor; eauto. Qed.
+End Forall2.
+
+Section Forall2_order.
+  Context  (R : relation A).
+
+  Global Instance: PreOrder R → PreOrder (Forall2 R).
+  Proof.
+    split.
+    * intros l. induction l; by constructor.
+    * intros l k k' Hlk. revert k'.
+      induction Hlk; inversion_clear 1; constructor.
+      + etransitivity; eauto.
+      + eauto.
+  Qed.
+End Forall2_order.
 End general_properties.
 
+Ltac decompose_elem_of_list := repeat
+  match goal with
+  | H : ?x ∈ [] |- _ => by destruct (not_elem_of_nil x)
+  | H : _ ∈ _ :: _ |- _ => apply elem_of_cons in H; destruct H
+  | H : _ ∈ _ ++ _ |- _ => apply elem_of_app in H; destruct H
+  end.
+Ltac decompose_Forall := repeat
+  match goal with
+  | H : Forall _ [] |- _ => clear H
+  | H : Forall _ (_ :: _) |- _ => apply Forall_inv in H; destruct H
+  | H : Forall _ (_ ++ _) |- _ => apply Forall_app in H; destruct H
+  end.
+
 (** * Theorems on the prefix and suffix predicates *)
 Section prefix_postfix.
-Context {A : Type}.
+  Context {A : Type}.
 
-Global Instance: PreOrder (@prefix_of A).
-Proof.
-  split.
-  * intros ?. eexists []. by rewrite app_nil_r.
-  * intros ??? [k1 ?] [k2 ?].
-    exists (k1 ++ k2). subst. by rewrite app_assoc.
-Qed.
+  Global Instance: PreOrder (@prefix_of A).
+  Proof.
+    split.
+    * intros ?. eexists []. by rewrite app_nil_r.
+    * intros ??? [k1 ?] [k2 ?].
+      exists (k1 ++ k2). subst. by rewrite app_assoc.
+  Qed.
 
-Lemma prefix_of_nil (l : list A) : prefix_of [] l.
-Proof. by exists l. Qed.
-Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) [].
-Proof. by intros [k E]. Qed.
-Lemma prefix_of_cons x y (l1 l2 : list A) :
-  x = y → prefix_of l1 l2 → prefix_of (x :: l1) (y :: l2).
-Proof. intros ? [k E]. exists k. by subst. Qed.
-Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) :
-  prefix_of (x :: l1) (y :: l2) → x = y.
-Proof. intros [k E]. by injection E. Qed.
-Lemma prefix_of_cons_inv_2 x y (l1 l2 : list A) :
-  prefix_of (x :: l1) (y :: l2) → prefix_of l1 l2.
-Proof. intros [k E]. exists k. by injection E. Qed.
-
-Lemma prefix_of_app_l (l1 l2 l3 : list A) :
-  prefix_of (l1 ++ l3) l2 → prefix_of l1 l2.
-Proof. intros [k ?]. red. exists (l3 ++ k). subst. by rewrite <-app_assoc. Qed.
-Lemma prefix_of_app_r (l1 l2 l3 : list A) :
-  prefix_of l1 l2 → prefix_of l1 (l2 ++ l3).
-Proof. intros [k ?]. exists (k ++ l3). subst. by rewrite app_assoc. Qed.
-
-Global Instance prefix_of_dec `{∀ x y : A, Decision (x = y)} :
-    ∀ l1 l2, Decision (prefix_of l1 l2) :=
-  fix prefix_of_dec l1 l2 :=
-  match l1, l2 return { prefix_of l1 l2 } + { ¬prefix_of l1 l2 } with
-  | [], _ => left (prefix_of_nil _)
-  | _, [] => right (prefix_of_nil_not _ _)
-  | x :: l1, y :: l2 =>
-    match decide_rel (=) x y with
-    | left Exy =>
-      match prefix_of_dec l1 l2 with
-      | left Hl1l2 => left (prefix_of_cons _ _ _ _ Exy Hl1l2)
-      | right Hl1l2 => right (Hl1l2 ∘ prefix_of_cons_inv_2 _ _ _ _)
-      end
-    | right Exy => right (Exy ∘ prefix_of_cons_inv_1 _ _ _ _)
-    end
-  end.
+  Lemma prefix_of_nil (l : list A) : prefix_of [] l.
+  Proof. by exists l. Qed.
+  Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) [].
+  Proof. by intros [k E]. Qed.
+  Lemma prefix_of_cons x y (l1 l2 : list A) :
+    x = y → prefix_of l1 l2 → prefix_of (x :: l1) (y :: l2).
+  Proof. intros ? [k E]. exists k. by subst. Qed.
+  Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) :
+    prefix_of (x :: l1) (y :: l2) → x = y.
+  Proof. intros [k E]. by injection E. Qed.
+  Lemma prefix_of_cons_inv_2 x y (l1 l2 : list A) :
+    prefix_of (x :: l1) (y :: l2) → prefix_of l1 l2.
+  Proof. intros [k E]. exists k. by injection E. Qed.
+
+  Lemma prefix_of_app_l (l1 l2 l3 : list A) :
+    prefix_of (l1 ++ l3) l2 → prefix_of l1 l2.
+  Proof. intros [k ?]. red. exists (l3 ++ k). subst. by rewrite <-app_assoc. Qed.
+  Lemma prefix_of_app_r (l1 l2 l3 : list A) :
+    prefix_of l1 l2 → prefix_of l1 (l2 ++ l3).
+  Proof. intros [k ?]. exists (k ++ l3). subst. by rewrite app_assoc. Qed.
+
+  Global Instance: PreOrder (@suffix_of A).
+  Proof.
+    split.
+    * intros ?. by eexists [].
+    * intros ??? [k1 ?] [k2 ?].
+      exists (k2 ++ k1). subst. by rewrite app_assoc.
+  Qed.
 
-Global Instance: PreOrder (@suffix_of A).
-Proof.
-  split.
-  * intros ?. by eexists [].
-  * intros ??? [k1 ?] [k2 ?].
-    exists (k2 ++ k1). subst. by rewrite app_assoc.
-Qed.
+  Lemma prefix_suffix_reverse (l1 l2 : list A) :
+    prefix_of l1 l2 ↔ suffix_of (reverse l1) (reverse l2).
+  Proof.
+    split; intros [k E]; exists (reverse k).
+    * by rewrite E, reverse_app.
+    * by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
+  Qed.
+  Lemma suffix_prefix_reverse (l1 l2 : list A) :
+    suffix_of l1 l2 ↔ prefix_of (reverse l1) (reverse l2).
+  Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
+
+  Lemma suffix_of_nil (l : list A) : suffix_of [] l.
+  Proof. exists l. by rewrite app_nil_r. Qed.
+  Lemma suffix_of_nil_inv (l : list A) : suffix_of l [] → l = [].
+  Proof. by intros [[|?] ?]; simplify_list_equality. Qed.
+  Lemma suffix_of_cons_nil_inv x (l : list A) : ¬suffix_of (x :: l) [].
+  Proof. by intros [[] ?]. Qed.
+
+  Lemma suffix_of_app (l1 l2 k : list A) :
+    suffix_of l1 l2 → suffix_of (l1 ++ k) (l2 ++ k).
+  Proof. intros [k' E]. exists k'. subst. by rewrite app_assoc. Qed.
+
+  Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) :
+    suffix_of (l1 ++ [x]) (l2 ++ [y]) → x = y.
+  Proof.
+    rewrite suffix_prefix_reverse, !reverse_snoc.
+    by apply prefix_of_cons_inv_1.
+  Qed.
+  Lemma suffix_of_snoc_inv_2 x y (l1 l2 : list A) :
+    suffix_of (l1 ++ [x]) (l2 ++ [y]) → suffix_of l1 l2.
+  Proof.
+    rewrite !suffix_prefix_reverse, !reverse_snoc.
+    by apply prefix_of_cons_inv_2.
+  Qed.
 
-Lemma prefix_suffix_reverse (l1 l2 : list A) :
-  prefix_of l1 l2 ↔ suffix_of (reverse l1) (reverse l2).
-Proof.
-  split; intros [k E]; exists (reverse k).
-  * by rewrite E, reverse_app.
-  * by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
-Qed.
-Lemma suffix_prefix_reverse (l1 l2 : list A) :
-  suffix_of l1 l2 ↔ prefix_of (reverse l1) (reverse l2).
-Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
-
-Lemma suffix_of_nil (l : list A) : suffix_of [] l.
-Proof. exists l. by rewrite app_nil_r. Qed.
-Lemma suffix_of_nil_inv (l : list A) : suffix_of l [] → l = [].
-Proof. by intros [[|?] ?]; simplify_list_equality. Qed.
-Lemma suffix_of_cons_nil_inv x (l : list A) : ¬suffix_of (x :: l) [].
-Proof. by intros [[] ?]. Qed.
-
-Lemma suffix_of_app (l1 l2 k : list A) :
-  suffix_of l1 l2 → suffix_of (l1 ++ k) (l2 ++ k).
-Proof. intros [k' E]. exists k'. subst. by rewrite app_assoc. Qed.
-
-Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) :
-  suffix_of (l1 ++ [x]) (l2 ++ [y]) → x = y.
-Proof.
-  rewrite suffix_prefix_reverse, !reverse_snoc.
-  by apply prefix_of_cons_inv_1.
-Qed.
-Lemma suffix_of_snoc_inv_2 x y (l1 l2 : list A) :
-  suffix_of (l1 ++ [x]) (l2 ++ [y]) → suffix_of l1 l2.
-Proof.
-  rewrite !suffix_prefix_reverse, !reverse_snoc.
-  by apply prefix_of_cons_inv_2.
-Qed.
+  Lemma suffix_of_cons_l (l1 l2 : list A) x :
+    suffix_of (x :: l1) l2 → suffix_of l1 l2.
+  Proof. intros [k ?]. exists (k ++ [x]). subst. by rewrite <-app_assoc. Qed.
+  Lemma suffix_of_app_l (l1 l2 l3 : list A) :
 
-Lemma suffix_of_cons_l (l1 l2 : list A) x :
-  suffix_of (x :: l1) l2 → suffix_of l1 l2.
-Proof. intros [k ?]. exists (k ++ [x]). subst. by rewrite <-app_assoc. Qed.
-Lemma suffix_of_app_l (l1 l2 l3 : list A) :
   suffix_of (l3 ++ l1) l2 → suffix_of l1 l2.
-Proof. intros [k ?]. exists (k ++ l3). subst. by rewrite <-app_assoc. Qed.
-Lemma suffix_of_cons_r (l1 l2 : list A) x :
-  suffix_of l1 l2 → suffix_of l1 (x :: l2).
-Proof. intros [k ?]. exists (x :: k). by subst. Qed.
-Lemma suffix_of_app_r (l1 l2 l3 : list A) :
-  suffix_of l1 l2 → suffix_of l1 (l3 ++ l2).
-Proof. intros [k ?]. exists (l3 ++ k). subst. by rewrite app_assoc. Qed.
-
-Lemma suffix_of_cons_inv (l1 l2 : list A) x y :
-  suffix_of (x :: l1) (y :: l2) →
-    x :: l1 = y :: l2 ∨ suffix_of (x :: l1) l2.
-Proof.
-  intros [[|? k] E].
-  * by left.
-  * right. simplify_equality. by apply suffix_of_app_r.
-Qed.
+  Proof. intros [k ?]. exists (k ++ l3). subst. by rewrite <-app_assoc. Qed.
+  Lemma suffix_of_cons_r (l1 l2 : list A) x :
+    suffix_of l1 l2 → suffix_of l1 (x :: l2).
+  Proof. intros [k ?]. exists (x :: k). by subst. Qed.
+  Lemma suffix_of_app_r (l1 l2 l3 : list A) :
+    suffix_of l1 l2 → suffix_of l1 (l3 ++ l2).
+  Proof. intros [k ?]. exists (l3 ++ k). subst. by rewrite app_assoc. Qed.
+
+  Lemma suffix_of_cons_inv (l1 l2 : list A) x y :
+    suffix_of (x :: l1) (y :: l2) →
+      x :: l1 = y :: l2 ∨ suffix_of (x :: l1) l2.
+  Proof.
+    intros [[|? k] E].
+    * by left.
+    * right. simplify_equality. by apply suffix_of_app_r.
+  Qed.
 
-Lemma suffix_of_cons_not x (l : list A) : ¬suffix_of (x :: l) l.
-Proof. intros [??]. discriminate_list_equality. Qed.
+  Lemma suffix_of_cons_not x (l : list A) : ¬suffix_of (x :: l) l.
+  Proof. intros [??]. discriminate_list_equality. Qed.
 
-Global Instance suffix_of_dec `{∀ x y : A, Decision (x = y)} (l1 l2 : list A) :
-  Decision (suffix_of l1 l2).
-Proof.
-  refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
-   abstract (by rewrite suffix_prefix_reverse).
-Defined.
+  Context `{∀ x y : A, Decision (x = y)}.
+
+  Fixpoint strip_prefix (l1 l2 : list A) : list A * (list A * list A) :=
+    match l1, l2 with
+    | [], l2 => ([], ([], l2))
+    | l1, [] => ([], (l1, []))
+    | x :: l1, y :: l2 =>
+      if decide_rel (=) x y
+      then fst_map (x ::) (strip_prefix l1 l2)
+      else ([], (x :: l1, y :: l2))
+    end.
+
+  Global Instance prefix_of_dec: ∀ l1 l2 : list A,
+      Decision (prefix_of l1 l2) :=
+    fix go l1 l2 :=
+    match l1, l2 return { prefix_of l1 l2 } + { ¬prefix_of l1 l2 } with
+    | [], _ => left (prefix_of_nil _)
+    | _, [] => right (prefix_of_nil_not _ _)
+    | x :: l1, y :: l2 =>
+      match decide_rel (=) x y with
+      | left Exy =>
+        match go l1 l2 with
+        | left Hl1l2 => left (prefix_of_cons _ _ _ _ Exy Hl1l2)
+        | right Hl1l2 => right (Hl1l2 ∘ prefix_of_cons_inv_2 _ _ _ _)
+        end
+      | right Exy => right (Exy ∘ prefix_of_cons_inv_1 _ _ _ _)
+      end
+    end.
+
+  Global Instance suffix_of_dec (l1 l2 : list A) :
+    Decision (suffix_of l1 l2).
+  Proof.
+    refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
+     abstract (by rewrite suffix_prefix_reverse).
+  Defined.
 End prefix_postfix.
 
-(** The [simplify_suffix_of] removes [suffix_of] hypotheses that are
+(** The [simplify_suffix_of] tactic removes [suffix_of] hypotheses that are
 tautologies, and simplifies [suffix_of] hypotheses involving [(::)] and
 [(++)]. *)
 Ltac simplify_suffix_of := repeat
@@ -503,8 +829,8 @@ Ltac simplify_suffix_of := repeat
   | _ => progress simplify_equality
   end.
 
-(** The [solve_suffix_of] tries to solve goals involving [suffix_of]. It uses
-[simplify_suffix_of] to simplify hypotheses and tries to solve [suffix_of]
+(** The [solve_suffix_of] tactic tries to solve goals involving [suffix_of]. It
+uses [simplify_suffix_of] to simplify hypotheses and tries to solve [suffix_of]
 conclusions. This tactic either fails or proves the goal. *)
 Ltac solve_suffix_of := solve [intuition (repeat
   match goal with
@@ -519,21 +845,59 @@ Ltac solve_suffix_of := solve [intuition (repeat
 Hint Extern 0 (PropHolds (suffix_of _ _)) =>
   unfold PropHolds; solve_suffix_of : typeclass_instances.
 
+(** * Folding lists *)
+Notation foldr := fold_right.
+Notation foldr_app := fold_right_app.
+
+Lemma foldr_permutation {A B} (R : relation B)
+   `{!Equivalence R}
+   (f : A → B → B) (b : B)
+   `{!Proper ((=) ==> R ==> R) f}
+   (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
+  Proper (Permutation ==> R) (foldr f b).
+Proof.
+  induction 1; simpl.
+  * done.
+  * by f_equiv.
+  * apply Hf.
+  * etransitivity; eauto.
+Qed.
+
+(** We redefine [foldl] with the arguments in the same order as in Haskell. *)
+Definition foldl {A B} (f : A → B → A) : A → list B → A :=
+  fix go a l :=
+  match l with
+  | [] => a
+  | x :: l => go (f a x) l
+  end.
+
+Lemma foldl_app {A B} (f : A → B → A) (l k : list B) (a : A) :
+  foldl f a (l ++ k) = foldl f (foldl f a l) k.
+Proof. revert a. induction l; simpl; auto. Qed.
+
 (** * Monadic operations *)
-Global Instance list_fmap {A B} (f : A → B) : FMap list f :=
+Instance list_ret: MRet list := λ A x, x :: @nil A.
+Instance list_fmap {A B} (f : A → B) : FMapD list f :=
   fix go (l : list A) :=
   match l with
   | [] => []
   | x :: l => f x :: @fmap _ _ _ f go l
   end.
-Global Instance list_join {A} : MJoin list :=
-  fix go (l : list (list A)) : list A :=
+Instance list_bind {A B} (f : A → list B) : MBindD list f :=
+  fix go (l : list A) :=
   match l with
-  | [] =>  []
-  | x :: l => x ++ @mjoin _ _ go l
+  | [] => []
+  | x :: l => f x ++ @mbind _ _ _ f go l
+  end.
+Instance list_join: MJoin list := λ A, mbind id.
+
+Definition mapM `{!MBind M} `{!MRet M} {A B}
+    (f : A → M B) : list A → M (list B) :=
+  fix go l :=
+  match l with
+  | [] => mret []
+  | x :: l => y ← f x; k ← go l; mret (y :: k)
   end.
-Global Instance list_bind {A B} (f : A → list B) : MBind list f := λ l,
-  mjoin (f <$> l).
 
 Section list_fmap.
   Context {A B : Type} (f : A → B).
@@ -570,29 +934,150 @@ Section list_fmap.
 
   Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
   Proof. revert i. induction l; by intros [|]. Qed.
-
-  Lemma in_fmap_1 l x : In x l → In (f x) (f <$> l).
-  Proof. induction l; destruct 1; subst; constructor (solve [auto]). Qed.
-  Lemma in_fmap_1_alt l x y : In x l → y = f x → In y (f <$> l).
-  Proof. intros. subst. by apply in_fmap_1. Qed.
-  Lemma in_fmap_2 l x : In x (f <$> l) → ∃ y, x = f y ∧ In y l.
+  Lemma list_alter_fmap (g : A → A) (h : B → B) l i :
+    Forall (λ x, f (g x) = h (f x)) l →
+    f <$> alter g i l = alter h i (f <$> l).
   Proof.
-    induction l as [|y l]; destruct 1; subst.
-    * exists y; by intuition.
-    * destruct IHl as [y' [??]]. done. exists y'; intuition.
+    intros Hl. revert i.
+    induction Hl; intros [|i]; simpl; f_equal; auto.
   Qed.
-  Lemma in_fmap l x : In x (f <$> l) ↔ ∃ y, x = f y ∧ In y l.
+  Lemma elem_of_list_fmap_1 l x : x ∈ l → f x ∈ f <$> l.
+  Proof. induction 1; simpl; rewrite elem_of_cons; intuition. Qed.
+  Lemma elem_of_list_fmap_1_alt l x y : x ∈ l → y = f x → y ∈ f <$> l.
+  Proof. intros. subst. by apply elem_of_list_fmap_1. Qed.
+  Lemma elem_of_list_fmap_2 l x : x ∈ f <$> l → ∃ y, x = f y ∧ y ∈ l.
   Proof.
-    split.
-    * apply in_fmap_2.
-    * intros [? [??]]. eauto using in_fmap_1_alt.
+    induction l as [|y l IH]; simpl; intros; decompose_elem_of_list.
+    + exists y. split; [done | by left].
+    + destruct IH as [z [??]]. done. exists z. split; [done | by right].
   Qed.
+  Lemma elem_of_list_fmap l x : x ∈ f <$> l ↔ ∃ y, x = f y ∧ y ∈  l.
+  Proof. firstorder eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2. Qed.
 
   Lemma Forall_fmap (l : list A) (P : B → Prop) :
-    Forall (P ∘ f) l ↔ Forall P (f <$> l).
-  Proof. induction l; split; inversion_clear 1; constructor; firstorder auto. Qed.
+    Forall P (f <$> l) ↔ Forall (P ∘ f) l.
+  Proof.
+    induction l; split; inversion_clear 1; constructor; firstorder auto.
+  Qed.
+
+  Lemma mapM_fmap (g : B → option A) (l : list A) :
+    (∀ x, g (f x) = Some x) →
+    mapM g (f <$> l) = Some l.
+  Proof.
+    intros E. induction l; simpl.
+    * done.
+    * by rewrite E, IHl.
+  Qed.
+  Lemma mapM_fmap_inv (g : B → option A) (l : list A) (k : list B) :
+    (∀ x y, g y = Some x → y = f x) →
+    mapM g k = Some l →
+    k = f <$> l.
+  Proof.
+    intros Hgf. revert l; induction k as [|y k]; intros [|x l] ?;
+      simplify_option_equality; f_equiv; eauto.
+  Qed.
 End list_fmap.
 
+Section list_bind.
+  Context {A B : Type} (f : A → list B).
+
+  Lemma bind_app (l1 l2 : list A) :
+    (l1 ++ l2) ≫= f = (l1 ≫= f) ++ (l2 ≫= f).
+  Proof.
+    induction l1; simpl; [done|].
+    by rewrite <-app_assoc, IHl1.
+  Qed.
+  Lemma elem_of_list_bind (x : B) (l : list A) :
+    x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
+  Proof.
+    split.
+    * induction l as [|y l IH]; simpl; intros; decompose_elem_of_list.
+      + exists y. split; [done | by left].
+      + destruct IH as [z [??]]. done.
+        exists z. split; [done | by right].
+    * intros [y [Hx Hy]].
+      induction Hy; simpl; rewrite elem_of_app; intuition.
+  Qed.
+End list_bind.
+
+Section list_ret_join.
+  Context {A : Type}.
+
+  Lemma elem_of_list_ret (x y : A) :
+    x ∈ @mret list _ A y ↔ x = y.
+  Proof. apply elem_of_list_singleton. Qed.
+  Lemma elem_of_list_join (x : A) (ll : list (list A)) :
+    x ∈ mjoin ll ↔ ∃ l, x ∈ l ∧ l ∈ ll.
+  Proof. unfold mjoin, list_join. by rewrite elem_of_list_bind. Qed.
+
+  Lemma join_nil (ls : list (list A)) :
+    mjoin ls = [] ↔ Forall (= nil) ls.
+  Proof.
+    unfold mjoin, list_join. split.
+    * by induction ls as [|[|??] ?]; constructor; auto.
+    * by induction 1 as [|[|??] ?].
+  Qed.
+  Lemma join_nil_1 (ls : list (list A)) :
+    mjoin ls = [] → Forall (= nil) ls.
+  Proof. by rewrite join_nil. Qed.
+  Lemma join_nil_2 (ls : list (list A)) :
+    Forall (= nil) ls → mjoin ls = [].
+  Proof. by rewrite join_nil. Qed.
+
+  Lemma join_length (ls : list (list A)) :
+    length (mjoin ls) = foldr (plus ∘ length) 0 ls.
+  Proof.
+    unfold mjoin, list_join.
+    by induction ls; simpl; rewrite ?app_length; f_equal.
+  Qed.
+  Lemma join_length_same (ls : list (list A)) n :
+    Forall (λ l, length l = n) ls →
+    length (mjoin ls) = length ls * n.
+  Proof. rewrite join_length. by induction 1; simpl; f_equal. Qed.
+
+  Lemma lookup_join_same_length (ls : list (list A)) n i :
+    n ≠ 0 →
+    Forall (λ l, length l = n) ls →
+    mjoin ls !! i = ls !! (i `div` n) ≫= (!! (i `mod` n)).
+  Proof.
+    intros Hn Hls. revert i. unfold mjoin, list_join.
+    induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
+    destruct (decide (i < n)) as [Hin|Hin].
+    * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
+      rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
+      simpl. rewrite lookup_app_l; auto with lia.
+    * replace i with ((i - n) + 1 * n) by lia.
+      rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
+      replace (i - n + 1 * n) with i by lia.
+      rewrite (plus_comm _ 1), lookup_app_r_alt, IH by lia.
+      by subst.
+  Qed.
+
+  (* This should be provable using the previous lemma in a shorter way *)
+  Lemma alter_join_same_length f (ls : list (list A)) n i :
+    n ≠ 0 →
+    Forall (λ l, length l = n) ls →
+    alter f i (mjoin ls) = mjoin (alter (alter f (i `mod` n)) (i `div` n) ls).
+  Proof.
+    intros Hn Hls. revert i. unfold mjoin, list_join.
+    induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
+    destruct (decide (i < n)) as [Hin|Hin].
+    * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
+      rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
+      simpl. rewrite alter_app_l; auto with lia.
+    * replace i with ((i - n) + 1 * n) by lia.
+      rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
+      replace (i - n + 1 * n) with i by lia.
+      rewrite (plus_comm _ 1), alter_app_r_alt, IH by lia.
+      by subst.
+  Qed.
+  Lemma insert_join_same_length (ls : list (list A)) n i x :
+    n ≠ 0 →
+    Forall (λ l, length l = n) ls →
+    <[i:=x]>(mjoin ls) = mjoin (alter <[i `mod` n:=x]> (i `div` n) ls).
+  Proof. apply alter_join_same_length. Qed.
+End list_ret_join.
+
 Ltac simplify_list_fmap_equality := repeat
   match goal with
   | _ => progress simplify_equality
@@ -654,7 +1139,7 @@ Section same_length.
     same_length l k → is_Some (l !! i) → is_Some (k !! i).
   Proof.
     rewrite same_length_length.
-    setoid_rewrite list_lookup_lt_length.
+    setoid_rewrite lookup_lt_length.
     intros E. by rewrite E.
   Qed.
 
@@ -675,38 +1160,89 @@ Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C :
   | _ , _ => []
   end.
 
-Notation zip := (zip_with pair).
+Section zip_with.
+  Context {A B C : Type} (f : A → B → C).
 
-Section zip.
-  Context {A B : Type}.
+  Lemma zip_with_length l1 l2 :
+    length l1 ≤ length l2 →
+    length (zip_with f l1 l2) = length l1.
+  Proof.
+    revert l2.
+    induction l1; intros [|??]; simpl; auto with lia.
+  Qed.
 
-  Lemma zip_fst_le (l1 : list A) (l2 : list B) :
-    length l1 ≤ length l2 → fst <$> zip l1 l2 = l1.
+  Lemma zip_with_fmap_fst_le (g : C → A) l1 l2 :
+    (∀ x y, g (f x y) = x) →
+    length l1 ≤ length l2 →
+    g <$> zip_with f l1 l2 = l1.
   Proof.
     revert l2.
-    induction l1; intros [|??] ?; simpl; f_equal; auto with arith.
-    edestruct Le.le_Sn_0; eauto.
+    induction l1; intros [|??] ??; simpl in *; f_equal; auto with lia.
   Qed.
-  Lemma zip_fst (l1 : list A) (l2 : list B) :
-    same_length l1 l2 → fst <$> zip l1 l2 = l1.
+  Lemma zip_with_fmap_snd_le (g : C → B) l1 l2 :
+    (∀ x y, g (f x y) = y) →
+    length l2 ≤ length l1 →
+    g <$> zip_with f l1 l2 = l2.
   Proof.
-    rewrite same_length_length. intros H.
-    apply zip_fst_le. by rewrite H.
+    revert l1.
+    induction l2; intros [|??] ??; simpl in *; f_equal; auto with lia.
+  Qed.
+  Lemma zip_with_fmap_fst (g : C → A) l1 l2 :
+    (∀ x y, g (f x y) = x) →
+    same_length l1 l2 →
+    g <$> zip_with f l1 l2 = l1.
+  Proof. induction 2; simpl; f_equal; auto. Qed.
+  Lemma zip_with_fmap_snd (g : C → B) l1 l2 :
+    (∀ x y, g (f x y) = y) →
+    same_length l1 l2 →
+    g <$> zip_with f l1 l2 = l2.
+  Proof. induction 2; simpl; f_equal; auto. Qed.
+
+  Lemma zip_with_Forall_fst (P : A → Prop) (Q : C → Prop) l1 l2 :
+    Forall P l1 →
+    Forall (λ y, ∀ x, P x → Q (f x y)) l2 →
+    Forall Q (zip_with f l1 l2).
+  Proof.
+    intros Hl1. revert l2.
+    induction Hl1; destruct 1; simpl in *; auto.
   Qed.
 
-  Lemma zip_snd_le (l1 : list A) (l2 : list B) :
-    length l2 ≤ length l1 → snd <$> zip l1 l2 = l2.
+  Lemma zip_with_Forall_snd (P : B → Prop) (Q : C → Prop) l1 l2 :
+    Forall (λ x, ∀ y, P y → Q (f x y)) l1 →
+    Forall P l2 →
+    Forall Q (zip_with f l1 l2).
   Proof.
-    revert l2.
-    induction l1; intros [|??] ?; simpl; f_equal; auto with arith.
-    edestruct Le.le_Sn_0; eauto.
+    intros Hl1. revert l2.
+    induction Hl1; destruct 1; simpl in *; auto.
   Qed.
+End zip_with.
+
+Notation zip := (zip_with pair).
+
+Section zip.
+  Context {A B : Type}.
+
+  Lemma zip_length (l1 : list A) (l2 : list B) :
+    length l1 ≤ length l2 →
+    length (zip l1 l2) = length l1.
+  Proof. by apply zip_with_length. Qed.
+
+  Lemma zip_fmap_fst_le (l1 : list A) (l2 : list B) :
+    length l1 ≤ length l2 →
+    fst <$> zip l1 l2 = l1.
+  Proof. by apply zip_with_fmap_fst_le. Qed.
+  Lemma zip_fmap_snd (l1 : list A) (l2 : list B) :
+    length l2 ≤ length l1 →
+    snd <$> zip l1 l2 = l2.
+  Proof. by apply zip_with_fmap_snd_le. Qed.
+
+  Lemma zip_fst (l1 : list A) (l2 : list B) :
+    same_length l1 l2 →
+    fst <$> zip l1 l2 = l1.
+  Proof. by apply zip_with_fmap_fst. Qed.
   Lemma zip_snd (l1 : list A) (l2 : list B) :
     same_length l1 l2 → snd <$> zip l1 l2 = l2.
-  Proof.
-    rewrite same_length_length. intros H.
-    apply zip_snd_le. by rewrite H.
-  Qed.
+  Proof. by apply zip_with_fmap_snd. Qed.
 End zip.
 
 Definition zipped_map {A B} (f : list A → list A → A → B) :
@@ -717,12 +1253,13 @@ Definition zipped_map {A B} (f : list A → list A → A → B) :
   | x :: k => f l k x :: go (x :: l) k
   end.
 
-Lemma In_zipped_map {A B} (f : list A → list A → A → B) l k x :
-  In x (zipped_map f l k) ↔
+Lemma elem_of_zipped_map {A B} (f : list A → list A → A → B) l k x :
+  x ∈ zipped_map f l k ↔
     ∃ k' k'' y, k = k' ++ [y] ++ k'' ∧ x = f (reverse k' ++ l) k'' y.
 Proof.
   split.
-  * revert l. induction k as [|z k IH]; [done | intros l [?|?]]; subst.
+  * revert l. induction k as [|z k IH]; simpl;
+      intros l ?; decompose_elem_of_list.
     + by eexists [], k, z.
     + destruct (IH (z :: l)) as [k' [k'' [y [??]]]]; [done |]; subst.
       eexists (z :: k'), k'', y. split; [done |].
@@ -762,3 +1299,54 @@ Proof.
   inversion_clear 1. rewrite reverse_cons, <-app_assoc.
   by apply IH.
 Qed.
+
+(** * Set operations on lists *)
+Section list_set_operations.
+  Context {A} {dec : ∀ x y : A, Decision (x = y)}.
+
+  Fixpoint list_difference (l k : list A) : list A :=
+    match l with
+    | [] => []
+    | x :: l =>
+      if decide_rel (∈) x k
+      then list_difference l k
+      else x :: list_difference l k
+    end.
+  Lemma elem_of_list_difference l k x :
+    x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k.
+  Proof.
+    split; induction l; simpl; try case_decide;
+      rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
+  Qed.
+  Lemma list_difference_nodup l k :
+    NoDup l → NoDup (list_difference l k).
+  Proof.
+    induction 1; simpl; try case_decide.
+    * constructor.
+    * done.
+    * constructor. rewrite elem_of_list_difference; intuition. done.
+  Qed.
+
+  Fixpoint list_intersection (l k : list A) : list A :=
+    match l with
+    | [] => []
+    | x :: l =>
+      if decide_rel (∈) x k
+      then x :: list_intersection l k
+      else list_intersection l k
+    end.
+  Lemma elem_of_list_intersection l k x :
+    x ∈ list_intersection l k ↔ x ∈ l ∧ x ∈ k.
+  Proof.
+    split; induction l; simpl; repeat case_decide;
+      rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
+  Qed.
+  Lemma list_intersection_nodup l k :
+    NoDup l → NoDup (list_intersection l k).
+  Proof.
+    induction 1; simpl; try case_decide.
+    * constructor.
+    * constructor. rewrite elem_of_list_intersection; intuition. done.
+    * done.
+  Qed.
+End list_set_operations.
diff --git a/theories/listset.v b/theories/listset.v
index 4405464c..eeb4d263 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -1,130 +1,95 @@
 (* Copyright (c) 2012, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
-(** This file implements finite as unordered lists without duplicates.
-Although this implementation is slow, it is very useful as decidable equality
-is the only constraint on the carrier set. *)
+(** This file implements finite as unordered lists without duplicates
+removed. This implementation forms a monad. *)
 Require Export base decidable collections list.
 
-Definition listset A := sig (@NoDup A).
+Record listset A := Listset {
+  listset_car: list A
+}.
+Arguments listset_car {_} _.
+Arguments Listset {_} _.
 
-Section list_collection.
-Context {A : Type} `{∀ x y : A, Decision (x = y)}.
+Section listset.
+Context {A : Type}.
 
-Global Instance listset_elem_of: ElemOf A (listset A) := λ x l, In x (`l).
-Global Instance listset_empty: Empty (listset A) := []↾@NoDup_nil _.
-Global Instance listset_singleton: Singleton A (listset A) := λ x,
-  [x]↾NoDup_singleton x.
+Instance listset_elem_of: ElemOf A (listset A) := λ x l,
+  x ∈ listset_car l.
+Instance listset_empty: Empty (listset A) :=
+  Listset [].
+Instance listset_singleton: Singleton A (listset A) := λ x,
+  Listset [x].
+Instance listset_union: Union (listset A) := λ l k,
+  Listset (listset_car l ++ listset_car k).
 
-Fixpoint listset_difference_raw (l k : list A) :=
-  match l with
-  | [] => []
-  | x :: l =>
-    if decide_rel In x k
-    then listset_difference_raw l k
-    else x :: listset_difference_raw l k
-  end.
-Lemma listset_difference_raw_in l k x :
-  In x (listset_difference_raw l k) ↔ In x l ∧ ¬In x k.
+Global Instance: SimpleCollection A (listset A).
 Proof.
-  split; induction l; simpl; try case_decide; simpl; intuition congruence.
-Qed.
-Lemma listset_difference_raw_nodup l k :
-  NoDup l → NoDup (listset_difference_raw l k).
-Proof.
-  induction 1; simpl; try case_decide.
-  * constructor.
-  * done.
-  * constructor. rewrite listset_difference_raw_in; intuition. done.
+  split.
+  * by apply not_elem_of_nil.
+  * by apply elem_of_list_singleton.
+  * intros. apply elem_of_app.
 Qed.
-Global Instance listset_difference: Difference (listset A) := λ l k,
-  listset_difference_raw (`l) (`k)↾
-    listset_difference_raw_nodup (`l) (`k) (proj2_sig l).
 
-Definition listset_union_raw (l k : list A) := listset_difference_raw l k ++ k.
-Lemma listset_union_raw_in l k x :
-  In x (listset_union_raw l k) ↔ In x l ∨ In x k.
-Proof.
-  unfold listset_union_raw. rewrite in_app_iff, listset_difference_raw_in.
-  intuition. case (decide (In x k)); intuition.
-Qed.
-Lemma listset_union_raw_nodup l k :
-  NoDup l → NoDup k → NoDup (listset_union_raw l k).
-Proof.
-  intros. apply NoDup_app.
-  * by apply listset_difference_raw_nodup.
-  * done.
-  * intro. rewrite listset_difference_raw_in. intuition.
-Qed.
-Global Instance listset_union: Union (listset A) := λ l k,
-  listset_union_raw (`l) (`k)↾
-    listset_union_raw_nodup (`l) (`k) (proj2_sig l) (proj2_sig k).
+Context `{∀ x y : A, Decision (x = y)}.
 
-Fixpoint listset_intersection_raw (l k : list A) :=
-  match l with
-  | [] => []
-  | x :: l =>
-    if decide_rel In x k
-    then x :: listset_intersection_raw l k
-    else listset_intersection_raw l k
-  end.
-Lemma listset_intersection_raw_in l k x :
-  In x (listset_intersection_raw l k) ↔ In x l ∧ In x k.
-Proof.
-  split; induction l; simpl; try case_decide; simpl; intuition congruence.
-Qed.
-Lemma listset_intersection_raw_nodup l k :
-  NoDup l → NoDup (listset_intersection_raw l k).
-Proof.
-  induction 1; simpl; try case_decide.
-  * constructor.
-  * constructor. rewrite listset_intersection_raw_in; intuition. done.
-  * done.
-Qed.
-Global Instance listset_intersection: Intersection (listset A) := λ l k,
-  listset_intersection_raw (`l) (`k)↾
-    listset_intersection_raw_nodup (`l) (`k) (proj2_sig l).
+Instance listset_intersection: Intersection (listset A) := λ l k,
+  Listset (list_intersection (listset_car l) (listset_car k)).
+Instance listset_difference: Difference (listset A) := λ l k,
+  Listset (list_difference (listset_car l) (listset_car k)).
 
-Definition listset_add_raw x (l : list A) : list A :=
-  if decide_rel In x l then l else x :: l.
-Lemma listset_add_raw_in x l y : In y (listset_add_raw x l) ↔ y = x ∨ In y l.
-Proof. unfold listset_add_raw. case_decide; firstorder congruence. Qed.
-Lemma listset_add_raw_nodup x l : NoDup l → NoDup (listset_add_raw x l).
+Global Instance: Collection A (listset A).
 Proof.
-  unfold listset_add_raw. case_decide; try constructor; firstorder.
+  split.
+  * apply _.
+  * intros. apply elem_of_list_intersection.
+  * intros. apply elem_of_list_difference.
 Qed.
 
-Fixpoint listset_map_raw (f : A → A) (l : list A) :=
-  match l with
-  | [] => []
-  | x :: l => listset_add_raw (f x) (listset_map_raw f l)
-  end.
-Lemma listset_map_raw_nodup f l : NoDup (listset_map_raw f l).
-Proof. induction l; simpl. constructor. by apply listset_add_raw_nodup. Qed.
-Lemma listset_map_raw_in f l x :
-  In x (listset_map_raw f l) ↔ ∃ y, x = f y ∧ In y l.
+Instance listset_elems: Elements A (listset A) :=
+  remove_dups ∘ listset_car.
+
+Global Instance: FinCollection A (listset A).
 Proof.
   split.
-  * induction l; simpl; [done |].
-    rewrite listset_add_raw_in. firstorder.
-  * intros [?[??]]. subst. induction l; simpl in *; [done |].
-    rewrite listset_add_raw_in. firstorder congruence.
+  * apply _.
+  * symmetry. apply elem_of_remove_dups.
+  * intros. apply remove_dups_nodup.
 Qed.
-Global Instance listset_map: Map A (listset A) := λ f l,
-  listset_map_raw f (`l)↾listset_map_raw_nodup f (`l).
+End listset.
 
-Global Instance: Collection A (listset A).
+(** These instances are declared using [Hint Extern] to avoid too
+eager type class search. *)
+Hint Extern 1 (ElemOf _ (listset _)) =>
+  eapply @listset_elem_of : typeclass_instances.
+Hint Extern 1 (Empty (listset _)) =>
+  eapply @listset_empty : typeclass_instances.
+Hint Extern 1 (Singleton _ (listset _)) =>
+  eapply @listset_singleton : typeclass_instances.
+Hint Extern 1 (Union (listset _)) =>
+  eapply @listset_union : typeclass_instances.
+Hint Extern 1 (Intersection (listset _)) =>
+  eapply @listset_intersection : typeclass_instances.
+Hint Extern 1 (Difference (listset _)) =>
+  eapply @listset_difference : typeclass_instances.
+Hint Extern 1 (Elements _ (listset _)) =>
+  eapply @listset_elems : typeclass_instances.
+
+Instance listset_ret: MRet listset := λ A x,
+  {[ x ]}.
+Instance listset_fmap: FMap listset := λ A B f l,
+  Listset (f <$> listset_car l).
+Instance listset_bind: MBind listset := λ A B f l,
+  Listset (mbind (listset_car ∘ f) (listset_car l)).
+Instance listset_join: MJoin listset := λ A, mbind id.
+
+Instance: CollectionMonad listset.
 Proof.
   split.
-  * intros ? [].
-  * compute. intuition.
-  * intros. apply listset_union_raw_in.
-  * intros. apply listset_intersection_raw_in.
-  * intros. apply listset_difference_raw_in.
-  * intros. apply listset_map_raw_in.
+  * intros. apply _.
+  * intros. apply elem_of_list_bind.
+  * intros. apply elem_of_list_ret.
+  * intros. apply elem_of_list_fmap.
+  * intros ?? [l].
+    unfold mjoin, listset_join, elem_of, listset_elem_of.
+    simpl. by rewrite elem_of_list_bind.
 Qed.
-
-Global Instance listset_elems: Elements A (listset A) := @proj1_sig _ _.
-
-Global Instance: FinCollection A (listset A).
-Proof. split. apply _. done. by intros [??]. Qed.
-End list_collection.
diff --git a/theories/nmap.v b/theories/nmap.v
index 2fbf85f3..210cfe03 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -7,40 +7,40 @@ Require Export prelude fin_maps.
 
 Local Open Scope N_scope.
 
-Record Nmap A := { Nmap_0 : option A; Nmap_pos : Pmap A }.
+Record Nmap A := NMap { Nmap_0 : option A; Nmap_pos : Pmap A }.
 Arguments Nmap_0 {_} _.
 Arguments Nmap_pos {_} _.
-Arguments Build_Nmap {_} _ _.
+Arguments NMap {_} _ _.
 
-Global Instance Pmap_dec `{∀ x y : A, Decision (x = y)} :
+Instance Pmap_dec `{∀ x y : A, Decision (x = y)} :
   ∀ x y : Nmap A, Decision (x = y).
 Proof. solve_decision. Defined.
 
-Global Instance Nempty {A} : Empty (Nmap A) := Build_Nmap None ∅.
-Global Instance Nlookup: Lookup N Nmap := λ A i t,
+Instance Nempty {A} : Empty (Nmap A) := NMap None ∅.
+Instance Nlookup {A} : Lookup N (Nmap A) A := λ i t,
   match i with
   | N0 => Nmap_0 t
   | Npos p => Nmap_pos t !! p
   end.
-Global Instance Npartial_alter: PartialAlter N Nmap := λ A f i t,
+Instance Npartial_alter {A} : PartialAlter N (Nmap A) A := λ f i t,
   match i, t with
-  | N0, Build_Nmap o t => Build_Nmap (f o) t
-  | Npos p, Build_Nmap o t => Build_Nmap o (partial_alter f p t)
+  | N0, NMap o t => NMap (f o) t
+  | Npos p, NMap o t => NMap o (partial_alter f p t)
   end.
-Global Instance Ndom: Dom N Nmap := λ C _ _ _ _ t,
+Instance Ndom {A} : Dom N (Nmap A) := λ C _ _ _ t,
   match t with
-  | Build_Nmap o t => option_case (λ _, {[ 0 ]}) ∅ o ∪ (Pdom_raw Npos (`t))
+  | NMap o t => option_case (λ _, {[ 0 ]}) ∅ o ∪ (Pdom_raw Npos (`t))
   end.
-Global Instance Nmerge: Merge Nmap := λ A f t1 t2,
+Instance Nmerge: Merge Nmap := λ A f t1 t2,
   match t1, t2 with
-  | Build_Nmap o1 t1, Build_Nmap o2 t2 => Build_Nmap (f o1 o2) (merge f t1 t2)
+  | NMap o1 t1, NMap o2 t2 => NMap (f o1 o2) (merge f t1 t2)
   end.
-Global Instance Nfmap {A B} (f : A → B) : FMap Nmap f := λ t,
+Instance Nfmap: FMap Nmap := λ A B f t,
   match t with
-  | Build_Nmap o t => Build_Nmap (fmap f o) (fmap f t)
+  | NMap o t => NMap (fmap f o) (fmap f t)
   end.
 
-Global Instance: FinMap N Nmap.
+Instance: FinMap N Nmap.
 Proof.
   split.
   * intros ? [??] [??] H. f_equal.
@@ -53,9 +53,9 @@ Proof.
   * intros ? f [? t] [|i] [|j]; simpl; try intuition congruence.
     intros. apply lookup_partial_alter_ne. congruence.
   * intros ??? [??] []; simpl. done. apply lookup_fmap.
-  * intros ?? ???????? [o t] n; simpl.
+  * intros ?? ??????? [o t] n; simpl.
     rewrite elem_of_union, Plookup_raw_dom.
-    destruct o, n; esolve_elem_of (simplify_is_Some; eauto).
+    destruct o, n; esolve_elem_of (inv_is_Some; eauto).
   * intros ? f ? [o1 t1] [o2 t2] [|?]; simpl.
     + done.
     + apply (merge_spec f t1 t2).
diff --git a/theories/numbers.v b/theories/numbers.v
index 4d09c4f8..8c39e4e8 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -6,8 +6,25 @@ notations. *)
 Require Export PArith NArith ZArith.
 Require Export base decidable.
 
+Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
+Reserved Notation "x ≤ y < z" (at level 70, y at next level).
+Reserved Notation "x < y < z" (at level 70, y at next level).
+Reserved Notation "x < y ≤ z" (at level 70, y at next level).
+
 Infix "≤" := le : nat_scope.
+Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%nat : nat_scope.
+Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%nat : nat_scope.
+Notation "x < y < z" := (x < y ∧ y < z)%nat : nat_scope.
+Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%nat : nat_scope.
+Notation "(≤)" := le (only parsing) : nat_scope.
+Notation "(<)" := lt (only parsing) : nat_scope.
+
+Infix "`div`" := NPeano.div (at level 35) : nat_scope.
+Infix "`mod`" := NPeano.modulo (at level 35) : nat_scope.
+
 Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
+Instance nat_le_dec: ∀ x y : nat, Decision (x ≤ y) := le_dec.
+Instance nat_lt_dec: ∀ x y : nat, Decision (x < y) := lt_dec.
 
 Lemma lt_n_SS n : n < S (S n).
 Proof. auto with arith. Qed.
@@ -19,9 +36,16 @@ Notation "(~0)" := xO (only parsing) : positive_scope.
 Notation "(~1)" := xI (only parsing) : positive_scope.
 
 Infix "≤" := N.le : N_scope.
+Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%N : N_scope.
+Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%N : N_scope.
+Notation "x < y < z" := (x < y ∧ y < z)%N : N_scope.
+Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%N : N_scope.
 Notation "(≤)" := N.le (only parsing) : N_scope.
 Notation "(<)" := N.lt (only parsing) : N_scope.
 
+Infix "`div`" := N.div (at level 35) : N_scope.
+Infix "`mod`" := N.modulo (at level 35) : N_scope.
+
 Instance N_eq_dec: ∀ x y : N, Decision (x = y) := N.eq_dec.
 Program Instance N_le_dec (x y : N) : Decision (x ≤ y)%N :=
   match Ncompare x y with
@@ -37,8 +61,13 @@ Program Instance N_lt_dec (x y : N) : Decision (x < y)%N :=
 Next Obligation. congruence. Qed.
 
 Infix "≤" := Z.le : Z_scope.
+Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%Z : Z_scope.
+Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%Z : Z_scope.
+Notation "x < y < z" := (x < y ∧ y < z)%Z : Z_scope.
+Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%Z : Z_scope.
 Notation "(≤)" := Z.le (only parsing) : Z_scope.
 Notation "(<)" := Z.lt (only parsing) : Z_scope.
+
 Instance Z_eq_dec: ∀ x y : Z, Decision (x = y) := Z.eq_dec.
 Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y)%Z := Z_le_dec.
 Instance Z_lt_dec: ∀ x y : Z, Decision (x < y)%Z := Z_lt_dec.
@@ -63,3 +92,61 @@ used for binary relations. It yields one if [R x y] and zero if not [R x y]. *)
 Definition Z_decide_rel {A B} (R : A → B → Prop)
     {dec : ∀ x y, Decision (R x y)} (x : A) (y : B) : Z :=
   (if dec x y then 1 else 0)%Z.
+
+(** Some correspondence lemmas between [nat] and [N] that are not part of the
+standard library. We declare a hint database [natify] to rewrite a goal
+involving [N] into a corresponding variant involving [nat]. *)
+Lemma N_to_nat_lt x y : N.to_nat x < N.to_nat y ↔ (x < y)%N.
+Proof. by rewrite <-N.compare_lt_iff, nat_compare_lt, N2Nat.inj_compare. Qed.
+Lemma N_to_nat_le x y : N.to_nat x ≤ N.to_nat y ↔ (x ≤ y)%N.
+Proof. by rewrite <-N.compare_le_iff, nat_compare_le, N2Nat.inj_compare. Qed.
+Lemma N_to_nat_0 : N.to_nat 0 = 0.
+Proof. done. Qed.
+Lemma N_to_nat_1 : N.to_nat 1 = 1.
+Proof. done. Qed.
+Lemma N_to_nat_div x y : N.to_nat (x `div` y) = N.to_nat x `div` N.to_nat y.
+Proof.
+  destruct (decide (y = 0%N)).
+  { subst. by destruct x. }
+  apply NPeano.Nat.div_unique with (N.to_nat (x `mod` y)).
+  { by apply N_to_nat_lt, N.mod_lt. }
+  rewrite (N.div_unique_exact (x * y) y x), N.div_mul by lia.
+  by rewrite <-N2Nat.inj_mul, <-N2Nat.inj_add, <-N.div_mod.
+Qed.
+(* We have [x `mod` 0 = 0] on [nat], and [x `mod` 0 = x] on [N]. *)
+Lemma N_to_nat_mod x y :
+  y ≠ 0%N →
+  N.to_nat (x `mod` y) = N.to_nat x `mod` N.to_nat y.
+Proof.
+  intros.
+  apply NPeano.Nat.mod_unique with (N.to_nat (x `div` y)).
+  { by apply N_to_nat_lt, N.mod_lt. }
+  rewrite (N.div_unique_exact (x * y) y x), N.div_mul by lia.
+  by rewrite <-N2Nat.inj_mul, <-N2Nat.inj_add, <-N.div_mod.
+Qed.
+
+Hint Rewrite <-N2Nat.inj_iff : natify.
+Hint Rewrite <-N_to_nat_lt : natify.
+Hint Rewrite <-N_to_nat_le : natify.
+Hint Rewrite Nat2N.id : natify.
+Hint Rewrite N2Nat.inj_add : natify.
+Hint Rewrite N2Nat.inj_mul : natify.
+Hint Rewrite N2Nat.inj_sub : natify.
+Hint Rewrite N2Nat.inj_succ : natify.
+Hint Rewrite N2Nat.inj_pred : natify.
+Hint Rewrite N_to_nat_div : natify.
+Hint Rewrite N_to_nat_0 : natify.
+Hint Rewrite N_to_nat_1 : natify.
+Ltac natify := repeat autorewrite with natify in *.
+
+Hint Extern 100 (Nlt _ _) => natify : natify.
+Hint Extern 100 (Nle _ _) => natify : natify.
+Hint Extern 100 (@eq N _ _) => natify : natify.
+Hint Extern 100 (lt _ _) => natify : natify.
+Hint Extern 100 (le _ _) => natify : natify.
+Hint Extern 100 (@eq nat _ _) => natify : natify.
+
+Instance: ∀ x, PropHolds (0 < x)%N → PropHolds (0 < N.to_nat x).
+Proof. unfold PropHolds. intros. by natify. Qed.
+Instance: ∀ x, PropHolds (0 ≤ x)%N → PropHolds (0 ≤ N.to_nat x).
+Proof. unfold PropHolds. intros. by natify. Qed.
diff --git a/theories/option.v b/theories/option.v
index 517b0d0a..3032b6f4 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -44,37 +44,44 @@ Proof.
   + done.
 Qed.
 
-(** We define [is_Some] as a [sig] instead of a [sigT] as extraction of
-witnesses can be derived (see [is_Some_sigT] below). *)
-Definition is_Some `(x : option A) : Prop := ∃ a, x = Some a.
-Hint Extern 10 (is_Some _) => solve [eexists; eauto].
+Inductive is_Some {A} : option A → Prop :=
+  make_is_Some x : is_Some (Some x).
 
-Ltac simplify_is_Some := repeat intro; repeat
+Lemma make_is_Some_alt `(x : option A) a : x = Some a → is_Some x.
+Proof. intros. by subst. Qed.
+Hint Resolve make_is_Some_alt.
+Lemma is_Some_None {A} : ¬is_Some (@None A).
+Proof. by inversion 1. Qed.
+Hint Resolve is_Some_None.
+
+Lemma is_Some_alt `(x : option A) : is_Some x ↔ ∃ y, x = Some y.
+Proof. split. inversion 1; eauto. intros [??]. by subst. Qed.
+
+Ltac inv_is_Some := repeat
   match goal with
-  | _ => progress simplify_equality
-  | H : is_Some _ |- _ => destruct H as [??]
-  | |- is_Some _ => eauto
+  | H : is_Some _ |- _ => inversion H; clear H; subst
   end.
 
-Lemma Some_is_Some `(a : A) : is_Some (Some a).
-Proof. simplify_is_Some. Qed.
-Lemma None_not_is_Some {A} : ¬is_Some (@None A).
-Proof. simplify_is_Some. Qed.
-
 Definition is_Some_sigT `(x : option A) : is_Some x → { a | x = Some a } :=
   match x with
-  | None => False_rect _ ∘ ex_ind None_ne_Some
-  | Some a => λ _, a↾eq_refl
+  | None => False_rect _ ∘ is_Some_None
+  | Some a => λ _, a ↾ eq_refl
+  end.
+
+Instance is_Some_dec `(x : option A) : Decision (is_Some x) :=
+  match x with
+  | Some x => left (make_is_Some x)
+  | None => right is_Some_None
   end.
-Lemma eq_Some_is_Some `(x : option A) a : x = Some a → is_Some x.
-Proof. simplify_is_Some. Qed.
 
 Lemma eq_None_not_Some `(x : option A) : x = None ↔ ¬is_Some x.
-Proof. destruct x; simpl; firstorder congruence. Qed.
+Proof. split. by destruct 2. destruct x. by intros []. done. Qed.
+Lemma not_eq_None_Some `(x : option A) : x ≠ None ↔ is_Some x.
+Proof. rewrite eq_None_not_Some. intuition auto using dec_stable. Qed.
 
 Lemma make_eq_Some {A} (x : option A) a :
   is_Some x → (∀ b, x = Some b → b = a) → x = Some a.
-Proof. intros [??] H. subst. f_equal. auto. Qed.
+Proof. destruct 1. intros. f_equal. auto. Qed.
 
 (** Equality on [option] is decidable. *)
 Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)}
@@ -97,26 +104,29 @@ Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)}
   end.
 
 (** * Monadic operations *)
-Instance option_bind {A B} (f : A → option B) : MBind option f := λ x,
+Instance option_ret: MRet option := @Some.
+Instance option_bind: MBind option := λ A B f x,
   match x with
   | Some a => f a
   | None => None
   end.
-Instance option_join {A} : MJoin option := λ x : option (option A),
+Instance option_join: MJoin option := λ A x,
   match x with
   | Some x => x
   | None => None
   end.
-Instance option_fmap {A B} (f : A → B) : FMap option f := option_map f.
+Instance option_fmap: FMap option := @option_map.
+Instance option_guard: MGuard option := λ P dec A x,
+  if dec then x else None.
 
 Lemma option_fmap_is_Some {A B} (f : A → B) (x : option A) :
   is_Some x ↔ is_Some (f <$> x).
-Proof. destruct x; split; intros [??]; subst; compute; by eauto. Qed.
+Proof. split; inversion 1. done. by destruct x. Qed.
 Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) :
   x = None ↔ f <$> x = None.
-Proof. unfold fmap, option_fmap. destruct x; simpl; split; congruence. Qed.
+Proof. unfold fmap, option_fmap. by destruct x. Qed.
 
-Tactic Notation "simplify_option_bind" "by" tactic3(tac) := repeat
+Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
   match goal with
   | _ => first [progress simpl in * | progress simplify_equality]
   | H : mbind (M:=option) (A:=?A) ?f ?o = ?x |- _ =>
@@ -135,8 +145,14 @@ Tactic Notation "simplify_option_bind" "by" tactic3(tac) := repeat
     let Hx := fresh in
     assert (o = Some x') as Hx by tac;
     rewrite Hx; clear Hx
+  | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ =>
+    let X := context C [ if dec then x else None ] in
+    change X in H; destruct dec
+  | |- context C [@mguard option _ ?P ?dec _ ?x] =>
+    let X := context C [ if dec then x else None ] in
+    change X; destruct dec
   end.
-Tactic Notation "simplify_option_bind" := simplify_option_bind by eauto.
+Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto.
 
 (** * Union, intersection and difference *)
 Instance option_union: UnionWith option := λ A f x y,
diff --git a/theories/orders.v b/theories/orders.v
index db32b3a2..f8014709 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -127,7 +127,8 @@ Section meet_sl.
   Proof. intros. transitivity x1; auto. Qed.
   Hint Resolve intersection_compat_l intersection_compat_r.
 
-  Lemma intersection_compat x1 x2 y1 y2 : x1 ⊆ x2 → y1 ⊆ y2 → x1 ∩ y1 ⊆ x2 ∩ y2.
+  Lemma intersection_compat x1 x2 y1 y2 :
+    x1 ⊆ x2 → y1 ⊆ y2 → x1 ∩ y1 ⊆ x2 ∩ y2.
   Proof. auto. Qed.
   Lemma intersection_comm x y : x ∩ y ⊆ y ∩ x.
   Proof. auto. Qed.
diff --git a/theories/pmap.v b/theories/pmap.v
index d6a54ad0..d8388187 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -57,10 +57,10 @@ Instance Pmap_wf_dec `(t : Pmap_raw A) : Decision (Pmap_wf t).
 Proof.
   red. induction t as [|l IHl [?|] r IHr]; simpl.
   * intuition.
-  * destruct IHl, IHr; try solve [left; intuition auto];
+  * destruct IHl, IHr; try solve [left; intuition];
       right; by inversion_clear 1.
   * destruct IHl, IHr, (decide (Pmap_ne l)), (decide (Pmap_ne r));
-      try solve [left; intuition auto];
+      try solve [left; intuition];
       right; inversion_clear 1; intuition.
 Qed.
 
@@ -77,20 +77,20 @@ Global Instance Pmap_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Pmap A) :
 
 Instance Pempty_raw {A} : Empty (Pmap_raw A) := Pleaf.
 Global Instance Pempty {A} : Empty (Pmap A) :=
-  (∅ : Pmap_raw A)↾bool_decide_pack _ Pmap_wf_leaf.
+  (∅ : Pmap_raw A) ↾ bool_decide_pack _ Pmap_wf_leaf.
 
-Instance Plookup_raw: Lookup positive Pmap_raw :=
-  fix Plookup_raw A (i : positive) (t : Pmap_raw A) {struct t} : option A :=
+Instance Plookup_raw {A} : Lookup positive (Pmap_raw A) A :=
+  fix Plookup_raw (i : positive) (t : Pmap_raw A) {struct t} : option A :=
   match t with
   | Pleaf => None
   | Pnode l o r =>
     match i with
     | 1 => o
-    | i~0 => @lookup _ _ Plookup_raw _ i l
-    | i~1 => @lookup _ _ Plookup_raw _ i r
+    | i~0 => @lookup _ _ _ Plookup_raw i l
+    | i~1 => @lookup _ _ _ Plookup_raw i r
     end
   end.
-Global Instance Plookup: Lookup positive Pmap := λ A i t, `t !! i.
+Instance Plookup {A} : Lookup positive (Pmap A) A := λ i t, `t !! i.
 
 Lemma Plookup_raw_empty {A} i : (∅ : Pmap_raw A) !! i = None.
 Proof. by destruct i. Qed.
@@ -179,9 +179,8 @@ Ltac Pnode_canon_rewrite := repeat (
   rewrite Pnode_canon_lookup_xO ||
   rewrite Pnode_canon_lookup_xI).
 
-Instance Ppartial_alter_raw: PartialAlter positive Pmap_raw :=
-  fix Ppartial_alter_raw A (f : option A → option A) (i : positive)
-    (t : Pmap_raw A) {struct t} : Pmap_raw A :=
+Instance Ppartial_alter_raw {A} : PartialAlter positive (Pmap_raw A) A :=
+  fix go f i t {struct t} : Pmap_raw A :=
   match t with
   | Pleaf =>
     match f None with
@@ -191,8 +190,8 @@ Instance Ppartial_alter_raw: PartialAlter positive Pmap_raw :=
   | Pnode l o r =>
     match i with
     | 1 => Pnode_canon l (f o) r
-    | i~0 => Pnode_canon (@partial_alter _ _ Ppartial_alter_raw _ f i l) o r
-    | i~1 => Pnode_canon l o (@partial_alter _ _ Ppartial_alter_raw _ f i r)
+    | i~0 => Pnode_canon (@partial_alter _ _ _ go f i l) o r
+    | i~1 => Pnode_canon l o (@partial_alter _ _ _ go f i r)
     end
   end.
 
@@ -205,14 +204,18 @@ Proof.
   * intros [?|?|]; simpl; intuition.
 Qed.
 
-Global Instance Ppartial_alter: PartialAlter positive Pmap := λ A f i t,
+Instance Ppartial_alter {A} : PartialAlter positive (Pmap A) A := λ f i t,
   dexist (partial_alter f i (`t)) (Ppartial_alter_raw_wf f i _ (proj2_dsig t)).
 
 Lemma Plookup_raw_alter {A} f i (t : Pmap_raw A) :
   partial_alter f i t !! i = f (t !! i).
 Proof.
   revert i. induction t.
-  * intros i. unfold partial_alter, lookup. simpl. case (f None).
+  * intros i. change (
+     match f None with
+     | Some x => Psingleton_raw i x
+     | None => Pleaf
+     end !! i = f None). destruct (f None).
     + intros. apply Plookup_raw_singleton.
     + by destruct i.
   * intros [?|?|]; simpl; by Pnode_canon_rewrite.
@@ -221,29 +224,33 @@ Lemma Plookup_raw_alter_ne {A} f i j (t : Pmap_raw A) :
   i ≠ j → partial_alter f i t !! j = t !! j.
 Proof.
   revert i j. induction t as [|l IHl ? r IHr].
-  * intros. unfold partial_alter, lookup. simpl. case (f None).
+  * intros. change (
+     match f None with
+     | Some x => Psingleton_raw i x
+     | None => Pleaf
+     end !! j = None). destruct (f None).
     + intros. by apply Plookup_raw_singleton_ne.
     + done.
   * intros [?|?|] [?|?|]; simpl; Pnode_canon_rewrite; auto; congruence.
 Qed.
 
-Instance Pfmap_raw {A B} (f : A → B) : FMap Pmap_raw f :=
-  fix Pfmap_raw (t : Pmap_raw A) : Pmap_raw B :=
+Instance Pfmap_raw {A B} (f : A → B) : FMapD Pmap_raw f :=
+  fix go (t : Pmap_raw A) : Pmap_raw B :=
+  let _ : FMapD Pmap_raw f := @go in
   match t with
   | Pleaf => Pleaf
-  | Pnode l x r =>
-    Pnode (@fmap _ _ _ f Pfmap_raw l) (fmap f x) (@fmap _ _ _ f Pfmap_raw r)
+  | Pnode l x r => Pnode (f <$> l) (f <$> x) (f <$> r)
   end.
 
 Lemma Pfmap_raw_ne `(f : A → B) (t : Pmap_raw A) :
   Pmap_ne t → Pmap_ne (fmap f t).
-Proof.  induction 1; simpl; auto. Qed.
+Proof. induction 1; simpl; auto. Qed.
 Local Hint Resolve Pfmap_raw_ne.
 Lemma Pfmap_raw_wf `(f : A → B) (t : Pmap_raw A) :
   Pmap_wf t → Pmap_wf (fmap f t).
-Proof. induction 1; simpl; intuition auto. Qed.
+Proof. induction 1; simpl; intuition. Qed.
 
-Global Instance Pfmap {A B} (f : A → B) : FMap Pmap f := λ t,
+Global Instance Pfmap {A B} (f : A → B) : FMapD Pmap f := λ t,
   dexist _ (Pfmap_raw_wf f _ (proj2_dsig t)).
 
 Lemma Plookup_raw_fmap `(f : A → B) (t : Pmap_raw A) i :
@@ -258,8 +265,9 @@ Section dom.
   Fixpoint Pdom_raw (f : positive → B) `(t : Pmap_raw A) : D :=
     match t with
     | Pleaf => ∅
-    | Pnode l o r => option_case (λ _, {[ f 1 ]}) ∅ o
-                       ∪ Pdom_raw (f ∘ (~0)) l ∪ Pdom_raw (f ∘ (~1)) r
+    | Pnode l o r =>
+       option_case (λ _, {[ f 1 ]}) ∅ o
+         ∪ Pdom_raw (f ∘ (~0)) l ∪ Pdom_raw (f ∘ (~1)) r
     end.
 
   Lemma Plookup_raw_dom f `(t : Pmap_raw A) x :
@@ -269,12 +277,14 @@ Section dom.
     * revert f. induction t as [|? IHl [?|] ? IHr]; esolve_elem_of.
     * intros [i [? Hlookup]]; subst. revert f i Hlookup.
       induction t as [|? IHl [?|] ? IHr]; intros f [?|?|];
-        solve_elem_of (by apply (IHl (f ∘ (~0)))
-        || by apply (IHr (f ∘ (~1))) || simplify_is_Some).
+       solve_elem_of (first
+        [ by apply (IHl (f ∘ (~0)))
+        | by apply (IHr (f ∘ (~1)))
+        | inv_is_Some; eauto ]).
   Qed.
 End dom.
 
-Global Instance Pdom : Dom positive Pmap := λ C _ _ _ _ t,
+Global Instance Pdom {A} : Dom positive (Pmap A) := λ C _ _ _ t,
   Pdom_raw id (`t).
 
 Fixpoint Pmerge_aux `(f : option A → option B) (t : Pmap_raw A) : Pmap_raw B :=
@@ -333,7 +343,7 @@ Proof.
   * intros ?? [??] ?. by apply Plookup_raw_alter.
   * intros ?? [??] ??. by apply Plookup_raw_alter_ne.
   * intros ??? [??]. by apply Plookup_raw_fmap.
-  * intros ?????????? [??] i. unfold dom, Pdom.
+  * intros ????????? [??] i. unfold dom, Pdom.
     rewrite Plookup_raw_dom. unfold id. split.
     + intros [? [??]]. by subst.
     + naive_solver.
diff --git a/theories/prelude.v b/theories/prelude.v
index 3712495c..27ea3b26 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -6,11 +6,11 @@ Require Export
   decidable
   orders
   option
-  list
   vector
   numbers
   collections
   fin_collections
   listset
-  subset
-  fresh_numbers.
+  listset_nodup
+  fresh_numbers
+  list.
diff --git a/theories/subset.v b/theories/subset.v
deleted file mode 100644
index b75ecc95..00000000
--- a/theories/subset.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* Copyright (c) 2012, Robbert Krebbers. *)
-(* This file is distributed under the terms of the BSD license. *)
-(** This file implements the operations on non computable subsets [A → Prop]
-over some carrier [A]. *)
-Require Export base.
-
-Definition subset A := A → Prop.
-
-Instance subset_elem_of {A} : ElemOf A (subset A) | 100 := λ x P, P x.
-Instance subset_empty {A} : Empty (subset A) := λ _, False.
-Instance subset_singleton {A} : Singleton A (subset A) := (=).
-Instance subset_union {A} : Union (subset A) := λ P Q x, P x ∨ Q x.
-Instance subset_intersection {A} : Intersection (subset A) := λ P Q x,
-  P x ∧ Q x.
-Instance subset_difference {A} : Difference (subset A) := λ P Q x, P x ∧ ¬Q x.
-Instance subset_map {A} : Map A (subset A) := λ f P x, ∃ y, f y = x ∧ P y.
-
-Instance subset_container: Collection A (subset A) | 100.
-Proof. firstorder congruence. Qed.
diff --git a/theories/tactics.v b/theories/tactics.v
index f29ec03f..96d24a41 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -2,8 +2,21 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects some general purpose tactics that are used throughout
 the development. *)
+Require Export Psatz.
 Require Export base.
 
+(** We declare hint databases [lia] and [congruence] containing solely the
+following hints. These hint database are useful in combination with another
+hint database [db] that contain lemmas with premises that should be solved by
+[lia] or [congruence]. One can now just say [auto with db,lia]. *)
+Hint Extern 1000 => lia : lia.
+Hint Extern 1000 => congruence : congruence.
+
+(** The tactic [intuition] expands to [intuition auto with *] by default. This
+is rather efficient when having big hint databases, or expensive [Hint Extern]
+declarations as the above. *)
+Tactic Notation "intuition" := intuition auto.
+
 (** A slightly modified version of Ssreflect's finishing tactic [done]. It
 also performs [reflexivity] and does not compute the goal's [hnf] so as to
 avoid unfolding setoid equalities. Note that this tactic performs much better
diff --git a/theories/vector.v b/theories/vector.v
index 101bfaab..20514323 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -251,11 +251,12 @@ Proof.
   apply vec_to_list_drop_lookup.
 Qed. 
 
-Lemma In_vlookup {A n} (v : vec A n) x :
-  In x (vec_to_list v) ↔ ∃ i, v !!! i = x.
+Lemma elem_of_vlookup {A n} (v : vec A n) x :
+  x ∈ vec_to_list v ↔ ∃ i, v !!! i = x.
 Proof.
   split.
-  * induction v; simpl; [done | intros [?|?]; subst].
+  * induction v; simpl; [by rewrite elem_of_nil |].
+    inversion 1; subst.
     + by eexists 0%fin.
     + destruct IHv as [i ?]; trivial. by exists (FS i).
   * intros [i ?]; subst. induction v; inv_fin i.
@@ -267,7 +268,7 @@ Lemma Forall_vlookup {A} (P : A → Prop) {n} (v : vec A n) :
   Forall P (vec_to_list v) ↔ ∀ i, P (v !!! i).
 Proof.
   rewrite Forall_forall.
-  setoid_rewrite In_vlookup. naive_solver.
+  setoid_rewrite elem_of_vlookup. naive_solver.
 Qed.
 Lemma Forall_vlookup_1 {A} (P : A → Prop) {n} (v : vec A n) i :
   Forall P (vec_to_list v) → P (v !!! i).
@@ -280,7 +281,7 @@ Lemma Exists_vlookup {A} (P : A → Prop) {n} (v : vec A n) :
   Exists P (vec_to_list v) ↔ ∃ i, P (v !!! i).
 Proof.
   rewrite Exists_exists.
-  setoid_rewrite In_vlookup. naive_solver.
+  setoid_rewrite elem_of_vlookup. naive_solver.
 Qed.
 
 Lemma Forall2_vlookup {A B} (P : A → B → Prop)
-- 
GitLab