diff --git a/theories/ars.v b/theories/ars.v
index 8cbb24b5b6f8c4c853bbbc247d744a5a7e63a58a..ba4a4df984dc0207f7e75cc74dff9327d2bc1a57 100644
--- a/theories/ars.v
+++ b/theories/ars.v
@@ -48,13 +48,15 @@ Hint Constructors rtc nsteps bsteps tc : ars.
 Section rtc.
   Context `{R : relation A}.
 
-  Global Instance: Reflexive (rtc R).
-  Proof rtc_refl R.
-  Global Instance rtc_trans: Transitive (rtc R).
-  Proof. red; induction 1; eauto with ars. Qed.
+  Instance rtc_preorder: PreOrder (rtc R).
+  Proof.
+    split.
+    * red. apply rtc_refl.
+    * red. induction 1; eauto with ars.
+  Qed.
   Lemma rtc_once x y : R x y → rtc R x y.
   Proof. eauto with ars. Qed.
-  Global Instance: subrelation R (rtc R).
+  Instance rtc_once_subrel: subrelation R (rtc R).
   Proof. exact @rtc_once. Qed.
   Lemma rtc_r x y z : rtc R x y → R y z → rtc R x z.
   Proof. intros. etransitivity; eauto with ars. Qed.
@@ -142,7 +144,7 @@ Section rtc.
   Proof. intros. etransitivity; eauto with ars. Qed.
   Lemma tc_rtc x y : tc R x y → rtc R x y.
   Proof. induction 1; eauto with ars. Qed.
-  Global Instance: subrelation (tc R) (rtc R).
+  Instance tc_once_subrel: subrelation (tc R) (rtc R).
   Proof. exact @tc_rtc. Qed.
 
   Lemma looping_red x : looping R x → red R x.
@@ -163,6 +165,14 @@ Section rtc.
   Qed.
 End rtc.
 
+(* Avoid too eager type class resolution *)
+Hint Extern 5 (subrelation _ (rtc _)) =>
+  eapply @rtc_once_subrel : typeclass_instances.
+Hint Extern 5 (subrelation _ (tc _)) =>
+  eapply @tc_once_subrel : typeclass_instances.
+Hint Extern 5 (PreOrder (rtc _)) =>
+  eapply @rtc_preorder : typeclass_instances.
+
 Hint Resolve
   rtc_once rtc_r
   tc_r
@@ -186,3 +196,35 @@ Section subrel.
   Global Instance tc_subrel: subrelation (tc R1) (tc R2).
   Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
 End subrel.
+
+Notation wf := well_founded.
+
+Section wf.
+  Context `{R : relation A}.
+
+  (** A trick by Thomas Braibant to compute with well-founded recursions:
+  it lazily adds [2^n] [Acc_intro] constructors in front of a well foundedness
+  proof, so that the actual proof is never reached in practise. *)
+  Fixpoint wf_guard (n : nat) (wfR : wf R) : wf R :=
+    match n with
+    | 0 => wfR
+    | S n => λ x, Acc_intro x (λ y _, wf_guard n (wf_guard n wfR) y)
+    end.
+
+  Lemma wf_projected `(R2 : relation B) (f : A → B) :
+    (∀ x y, R x y → R2 (f x) (f y)) →
+    wf R2 → wf R.
+  Proof.
+    intros Hf Hwf.
+    cut (∀ y, Acc R2 y → ∀ x, y = f x → Acc R x).
+    { intros aux x. apply (aux (f x)); auto. }
+    induction 1 as [y _ IH]. intros x ?. subst.
+    constructor. intros. apply (IH (f y)); auto.
+  Qed.
+End wf.
+
+(* Generally we do not want [wf_guard] to be expanded (neither by tactics,
+nor by conversion tests in the kernel), but in some cases we do need it for
+computation (that is, we cannot make it opaque). We use the [Strategy]
+command to make its expanding behavior less eager. *)
+Strategy 100 [wf_guard].
diff --git a/theories/base.v b/theories/base.v
index 4ddd3a76bfaaa06c7dcf58bfe4af145eaea3c6e9..f810734d034e393a9e6774545016a16a974f939c 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -12,9 +12,11 @@ Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid NArith.
 (** The following coercion allows us to use Booleans as propositions. *)
 Coercion Is_true : bool >-> Sortclass.
 
-(** Ensure that [simpl] unfolds [id] and [compose] when fully applied. *)
+(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
+applied. *)
 Arguments id _ _/.
 Arguments compose _ _ _ _ _ _ /.
+Arguments flip _ _ _ _ _ _/.
 
 (** Change [True] and [False] into notations in order to enable overloading.
 We will use this in the file [assertions] to give [True] and [False] a
@@ -23,6 +25,9 @@ semantics. *)
 Notation "'True'" := True : type_scope.
 Notation "'False'" := False : type_scope.
 
+Notation curry := prod_curry.
+Notation uncurry := prod_uncurry.
+
 (** Throughout this development we use [C_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
 Delimit Scope C_scope with C.
@@ -159,6 +164,17 @@ Notation "( ⊈ X )" := (λ Y, Y ⊈ X) (only parsing) : C_scope.
 
 Hint Extern 0 (_ ⊆ _) => reflexivity.
 
+Class Subset A := subset: A → A → Prop.
+Instance: Params (@subset) 2.
+Infix "⊂" := subset (at level 70) : C_scope.
+Notation "(⊂)" := subset (only parsing) : C_scope.
+Notation "( X ⊂ )" := (subset X) (only parsing) : C_scope.
+Notation "( ⊂ X )" := (λ Y, subset Y X) (only parsing) : C_scope.
+Notation "X ⊄  Y" := (¬X ⊂ Y) (at level 70) : C_scope.
+Notation "(⊄)" := (λ X Y, X ⊄ Y) (only parsing) : C_scope.
+Notation "( X ⊄ )" := (λ Y, X ⊄ Y) (only parsing) : C_scope.
+Notation "( ⊄ X )" := (λ Y, Y ⊄ X) (only parsing) : C_scope.
+
 Class ElemOf A B := elem_of: A → B → Prop.
 Instance: Params (@elem_of) 3.
 Infix "∈" := elem_of (at level 70) : C_scope.
@@ -192,6 +208,10 @@ Proof. inversion_clear 1; auto. Qed.
 Instance generic_disjoint `{ElemOf A B} : Disjoint B | 100 :=
   λ X Y, ∀ x, x ∉ X ∨ x ∉ Y.
 
+Class Filter A B :=
+  filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B.
+(* Arguments filter {_ _ _} _ {_} !_ / : simpl nomatch. *)
+
 (** ** 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
@@ -230,9 +250,13 @@ Instance: Params (@fmap) 6.
 Arguments fmap {_ _ _} _ {_} !_ / : simpl nomatch.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
+Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : C_scope.
+Notation "(≫= f )" := (mbind f) (only parsing) : C_scope.
+Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : 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.
+Infix "<$>" := fmap (at level 65, right associativity) : C_scope.
 
 Class MGuard (M : Type → Type) :=
   mguard: ∀ P {dec : Decision P} {A}, M A → M A.
@@ -243,7 +267,7 @@ Notation "'guard' P ; o" := (mguard P o)
 (** 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 M A : Type) :=
+Class Lookup (K A M : Type) :=
   lookup: K → M → option A.
 Instance: Params (@lookup) 4.
 
@@ -255,7 +279,7 @@ 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 M A : Type) :=
+Class Insert (K A M : Type) :=
   insert: K → A → M → M.
 Instance: Params (@insert) 4.
 Notation "<[ k := a ]>" := (insert k a)
@@ -272,9 +296,9 @@ 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 AlterD (K M A : Type) (f : A → A) :=
+Class AlterD (K A M : Type) (f : A → A) :=
   alter: K → M → M.
-Notation Alter K M A := (∀ (f : A → A), AlterD K M A f)%type.
+Notation Alter K A M := (∀ (f : A → A), AlterD K A M f)%type.
 Instance: Params (@alter) 5.
 Arguments alter {_ _ _} _ {_} !_ !_ / : simpl nomatch.
 
@@ -282,7 +306,7 @@ Arguments alter {_ _ _} _ {_} !_ !_ / : simpl nomatch.
 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 M A : Type) :=
+Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
 Instance: Params (@partial_alter) 4.
 Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
@@ -297,39 +321,43 @@ 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)]
 provided that [k] is a member of either [m1] or [m2].*)
-Class Merge (M : Type → Type) :=
-  merge: ∀ {A}, (option A → option A → option A) → M A → M A → M A.
+Class Merge (A M : Type) :=
+  merge: (option A → option A → option A) → M → M → M.
 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) : M :=
+Definition insert_list `{Insert K A M} (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} (l : list K) (m : M) : M :=
   fold_right delete m l.
 Instance: Params (@delete_list) 3.
 
-Definition insert_consecutive `{Insert nat M A}
+Definition insert_consecutive `{Insert nat A M}
     (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
-[m2]. *)
-Class UnionWith (M : Type → Type) :=
-  union_with: ∀ {A}, (A → A → A) → M A → M A → M A.
+(** The function [union_with f m1 m2] is supposed to yield the union of [m1]
+and [m2] using the function [f] to combine values of members that are in
+both [m1] and [m2]. *)
+Class UnionWith (A M : Type) :=
+  union_with: (A → A → option A) → M → M → M.
 Instance: Params (@union_with) 3.
 
-(** Similarly for the intersection and difference. *)
-Class IntersectionWith (M : Type → Type) :=
-  intersection_with: ∀ {A}, (A → A → A) → M A → M A → M A.
+(** Similarly for intersection and difference. *)
+Class IntersectionWith (A M : Type) :=
+  intersection_with: (A → A → option A) → M → M → M.
 Instance: Params (@intersection_with) 3.
-Class DifferenceWith (M : Type → Type) :=
-  difference_with: ∀ {A}, (A → A → option A) → M A → M A → M A.
+Class DifferenceWith (A M : Type) :=
+  difference_with: (A → A → option A) → M → M → M.
 Instance: Params (@difference_with) 3.
 
+Definition intersection_with_list `{IntersectionWith A M}
+  (f : A → A → option A) : M → list M → M := fold_right (intersection_with f).
+Arguments intersection_with_list _ _ _ _ _ !_ /.
+
 (** ** Common properties *)
 (** These operational type classes allow us to refer to common mathematical
 properties in a generic way. For example, for injectivity of [(k ++)] it
@@ -350,6 +378,8 @@ Class LeftAbsorb {A} R (i : A) (f : A → A → A) :=
   left_absorb: ∀ x, R (f i x) i.
 Class RightAbsorb {A} R (i : A) (f : A → A → A) :=
   right_absorb: ∀ x, R (f x i) i.
+Class AntiSymmetric {A} (R : A → A → Prop) :=
+  anti_symmetric: ∀ x y, R x y → R y x → x = y.
 
 Arguments injective {_ _ _ _} _ {_} _ _ _.
 Arguments idempotent {_ _} _ {_} _.
@@ -359,6 +389,7 @@ Arguments right_id {_ _} _ _ {_} _.
 Arguments associative {_ _} _ {_} _ _ _.
 Arguments left_absorb {_ _} _ _ {_} _.
 Arguments right_absorb {_ _} _ _ {_} _.
+Arguments anti_symmetric {_} _ {_} _ _ _ _.
 
 (** The following lemmas are more specific versions of the projections of the
 above type classes. These lemmas allow us to enforce Coq not to use the setoid
@@ -391,6 +422,10 @@ Class BoundedPreOrder A `{Empty A} `{SubsetEq A} := {
   bounded_preorder :>> PreOrder (⊆);
   subseteq_empty x : ∅ ⊆ x
 }.
+Class PartialOrder A `{SubsetEq A} := {
+  po_preorder :>> PreOrder (⊆);
+  po_antisym :> AntiSymmetric (⊆)
+}.
 
 (** We do not include equality in the following interfaces so as to avoid the
 need for proofs that the  relations and operations respect setoid equality.
@@ -423,11 +458,13 @@ Class SimpleCollection A C `{ElemOf A C}
   elem_of_singleton (x y : A) : x ∈ {[ y ]} ↔ 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} := {
+Class Collection A C `{ElemOf A C} `{Empty C} `{Singleton A C}
+    `{Union C} `{Intersection C} `{Difference C} `{IntersectionWith A 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_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y;
+  elem_of_intersection_with (f : A → A → option A) X Y (x : A) :
+    x ∈ intersection_with f X Y ↔ ∃ x1 x2, x1 ∈ X ∧ x2 ∈ Y ∧ f x1 x2 = Some x
 }.
 
 (** We axiomative a finite collection as a collection whose elements can be
@@ -448,10 +485,12 @@ Inductive NoDup {A} : list A → Prop :=
 
 (** 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}
-    `{Elements A C} `{∀ x y : A, Decision (x = y)} := {
+Class FinCollection A C `{ElemOf A C} `{Empty C} `{Singleton A C}
+    `{Union C} `{Intersection C} `{Difference C} `{IntersectionWith A C}
+    `{Filter A C} `{Elements A C} `{∀ x y : A, Decision (x = y)} := {
   fin_collection :>> Collection A C;
+  elem_of_filter X P `{∀ x, Decision (P x)} x :
+    x ∈ filter P X ↔ P x ∧ x ∈ X;
   elements_spec X x : x ∈ X ↔ x ∈ elements X;
   elements_nodup X : NoDup (elements X)
 }.
@@ -471,13 +510,13 @@ 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) :
+  elem_of_bind {A B} (f : A → M B) (X : M A) (x : B) :
     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) :
+  elem_of_fmap {A B} (f : A → B) (X : M A) (x : B) :
     x ∈ f <$> X ↔ ∃ y, x = f y ∧ y ∈ X;
-  elem_of_join {A} (x : A) (X : M (M A)) :
+  elem_of_join {A} (X : M (M A)) (x : A) :
     x ∈ mjoin X ↔ ∃ Y, x ∈ Y ∧ Y ∈ X
 }.
 
@@ -520,6 +559,24 @@ Definition fst_map {A A' B} (f : A → A') (p : A * B) : A' * B :=
   (f (fst p), snd p).
 Definition snd_map {A B B'} (f : B → B') (p : A * B) : A * B' :=
   (fst p, f (snd p)).
+Arguments fst_map {_ _ _} _ !_ /.
+Arguments snd_map {_ _ _} _ !_ /.
+
+Instance: ∀ {A A' B} (f : A → A'),
+  Injective (=) (=) f → Injective (=) (=) (@fst_map A A' B f).
+Proof.
+  intros ????? [??] [??]; simpl; intro; f_equal.
+  * apply (injective f). congruence.
+  * congruence.
+Qed.
+Instance: ∀ {A B B'} (f : B → B'),
+  Injective (=) (=) f → Injective (=) (=) (@snd_map A B B' f).
+Proof.
+  intros ????? [??] [??]; simpl; intro; f_equal.
+  * congruence.
+  * apply (injective f). congruence.
+Qed.
+
 Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
   relation (A * B) := λ x y, R1 (fst x) (fst y) ∧ R2 (snd x) (snd y).
 
diff --git a/theories/collections.v b/theories/collections.v
index 9013df374ddbe5fb74fe356b6c0e795c0bb1721f..b96b6836cd89a3c643b5cd559c8e2f92c0b068ae 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -39,7 +39,7 @@ Section simple_collection.
   Global Instance elem_of_proper: Proper ((=) ==> (≡) ==> iff) (∈) | 5.
   Proof. intros ???. subst. firstorder. Qed.
 
-  Lemma elem_of_union_list (x : A) (Xs : list C) :
+  Lemma elem_of_union_list (Xs : list C) (x : A) :
     x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
   Proof.
     split.
@@ -60,7 +60,7 @@ Section simple_collection.
   Lemma not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
   Proof. rewrite elem_of_union. tauto. Qed.
 
-  Context `{∀ (X Y : C), Decision (X ⊆ Y)}.
+  Context `{∀ X Y : C, Decision (X ⊆ Y)}.
 
   Global Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
   Proof.
@@ -69,37 +69,6 @@ Section simple_collection.
   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.
-    rewrite elem_of_intersection.
-    destruct (decide (x ∈ X)); tauto.
-  Qed.
-  Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y.
-  Proof.
-    rewrite elem_of_difference.
-    destruct (decide (x ∈ Y)); tauto.
-  Qed.
-  Lemma union_difference X Y : X ∪ Y ∖ X ≡ X ∪ Y.
-  Proof.
-    split; intros x; rewrite !elem_of_union, elem_of_difference.
-    * tauto.
-    * destruct (decide (x ∈ X)); tauto.
-  Qed.
-End collection.
-
 Ltac decompose_empty := repeat
   match goal with
   | H : _ ∪ _ ≡ ∅ |- _ => apply empty_union in H; destruct H
@@ -116,6 +85,7 @@ Ltac unfold_elem_of :=
   repeat_on_hyps (fun H =>
     repeat match type of H with
     | context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq in H
+    | context [ _ ⊂ _ ] => setoid_rewrite subset_spec in H
     | context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt in H
     | context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty in H
     | context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton in H
@@ -129,6 +99,7 @@ Ltac unfold_elem_of :=
     end);
   repeat match goal with
   | |- context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq
+  | |- context [ _ ⊂ _ ] => setoid_rewrite subset_spec
   | |- context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt
   | |- context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty
   | |- context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton
@@ -194,6 +165,79 @@ Tactic Notation "decompose_elem_of" hyp(H) :=
 Tactic Notation "decompose_elem_of" :=
   repeat_on_hyps (fun H => decompose_elem_of H).
 
+Section collection.
+  Context `{Collection A C}.
+
+  Global Instance: LowerBoundedLattice C.
+  Proof. split. apply _. firstorder auto. Qed.
+
+  Lemma intersection_singletons x : {[x]} ∩ {[x]} ≡ {[x]}.
+  Proof. esolve_elem_of. Qed.
+  Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y.
+  Proof. esolve_elem_of. Qed.
+
+  Lemma empty_difference X Y : X ⊆ Y → X ∖ Y ≡ ∅.
+  Proof. esolve_elem_of. Qed.
+  Lemma difference_diag X : X ∖ X ≡ ∅.
+  Proof. esolve_elem_of. Qed.
+  Lemma difference_union_distr_l X Y Z : (X ∪ Y) ∖ Z ≡ X ∖ Z ∪ Y ∖ Z.
+  Proof. esolve_elem_of. Qed.
+  Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z.
+  Proof. esolve_elem_of. Qed.
+
+  Lemma elem_of_intersection_with_list (f : A → A → option A) Xs Y x :
+    x ∈ intersection_with_list f Y Xs ↔ ∃ xs y,
+      Forall2 (∈) xs Xs ∧ y ∈ Y ∧ foldr (λ x, (≫= f x)) (Some y) xs = Some x.
+  Proof.
+    split.
+    * revert x. induction Xs; simpl; intros x HXs.
+      + eexists [], x. intuition.
+      + rewrite elem_of_intersection_with in HXs.
+        destruct HXs as (x1 & x2 & Hx1 & Hx2 & ?).
+        destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial.
+        eexists (x1 :: xs), y. intuition (simplify_option_equality; auto).
+    * intros (xs & y & Hxs & ? & Hx). revert x Hx.
+      induction Hxs; intros; simplify_option_equality; [done |].
+      rewrite elem_of_intersection_with. naive_solver.
+  Qed.
+
+  Lemma intersection_with_list_ind (P Q : A → Prop) f Xs Y :
+    (∀ y, y ∈ Y → P y) →
+    Forall (λ X, ∀ x, x ∈ X → Q x) Xs →
+    (∀ x y z, Q x → P y → f x y = Some z → P z) →
+    ∀ x, x ∈ intersection_with_list f Y Xs → P x.
+  Proof.
+    intros HY HXs Hf.
+    induction Xs; simplify_option_equality; [done |].
+    intros x Hx. rewrite elem_of_intersection_with in Hx.
+    decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto.
+  Qed.
+
+  Context `{∀ X Y : C, Decision (X ⊆ Y)}.
+
+  Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
+  Proof.
+    rewrite elem_of_intersection.
+    destruct (decide (x ∈ X)); tauto.
+  Qed.
+  Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y.
+  Proof.
+    rewrite elem_of_difference.
+    destruct (decide (x ∈ Y)); tauto.
+  Qed.
+  Lemma union_difference X Y : X ⊆ Y → Y ≡ X ∪ Y ∖ X.
+  Proof.
+    split; intros x; rewrite !elem_of_union, elem_of_difference.
+    * destruct (decide (x ∈ X)); intuition.
+    * intuition.
+  Qed.
+  Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅.
+  Proof.
+    intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x.
+    destruct (decide (x ∈ X)); esolve_elem_of.
+  Qed.
+End collection.
+
 (** * Sets without duplicates up to an equivalence *)
 Section no_dup.
   Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}.
@@ -202,7 +246,7 @@ Section no_dup.
   Definition no_dup (X : B) := ∀ x y, x ∈ X → y ∈ X → R x y → x = y.
 
   Global Instance: Proper ((≡) ==> iff) (elem_of_upto x).
-  Proof. firstorder. Qed.
+  Proof. intros ??? E. unfold elem_of_upto. by setoid_rewrite E. Qed.
   Global Instance: Proper (R ==> (≡) ==> iff) elem_of_upto.
   Proof.
     intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
@@ -390,10 +434,13 @@ Section collection_monad.
     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.
+  Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed.
+  Lemma elem_of_mapM_Forall2_l {A B C} (f : A → M B) (P : B → C → Prop) l1 l2 k :
+    l1 ∈ mapM f k →
+    Forall2 (λ x y, ∀ z, z ∈ f x → P z y) k l2 →
+    Forall2 P l1 l2.
+  Proof.
+    rewrite elem_of_mapM. intros Hl1. revert l2.
+    induction Hl1; inversion_clear 1; constructor; auto.
+  Qed.
 End collection_monad.
diff --git a/theories/decidable.v b/theories/decidable.v
index 3ed33cb30df594cb08865ec39e97577e8493b471..9ea1ccbd5cbf37456ee90720aa775cb41d89c666 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -5,6 +5,8 @@ with a decidable equality. Such propositions are collected by the [Decision]
 type class. *)
 Require Export base tactics.
 
+Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances.
+
 Lemma dec_stable `{Decision P} : ¬¬P → P.
 Proof. firstorder. Qed.
 
@@ -82,6 +84,8 @@ combination with the [refine] tactic. *)
 Notation cast_if S := (if S then left _ else right _).
 Notation cast_if_and S1 S2 := (if S1 then cast_if S2 else right _).
 Notation cast_if_and3 S1 S2 S3 := (if S1 then cast_if_and S2 S3 else right _).
+Notation cast_if_and4 S1 S2 S3 S4 :=
+  (if S1 then cast_if_and3 S2 S3 S4 else right _).
 Notation cast_if_or S1 S2 := (if S1 then left _ else cast_if S2).
 Notation cast_if_not S := (if S then right _ else left _).
 
@@ -104,14 +108,24 @@ Section prop_dec.
 End prop_dec.
 
 (** Instances of [Decision] for common data types. *)
+Instance bool_eq_dec (x y : bool) : Decision (x = y).
+Proof. solve_decision. Defined.
 Instance unit_eq_dec (x y : unit) : Decision (x = y).
 Proof. refine (left _); by destruct x, y. Defined.
 Instance prod_eq_dec `(A_dec : ∀ x y : A, Decision (x = y))
-    `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A * B) : Decision (x = y).
+  `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A * B) : Decision (x = y).
 Proof.
   refine (cast_if_and (A_dec (fst x) (fst y)) (B_dec (snd x) (snd y)));
     abstract (destruct x, y; simpl in *; congruence).
 Defined.
 Instance sum_eq_dec `(A_dec : ∀ x y : A, Decision (x = y))
-    `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A + B) : Decision (x = y).
+  `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A + B) : Decision (x = y).
 Proof. solve_decision. Defined.
+
+Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
+    Decision (curry P p) :=
+  match p as p return Decision (curry P p) with
+  | (x,y) => P_dec x y
+  end.
+Instance uncurry_dec `(P_dec : ∀ (p : A * B), Decision (P p)) x y :
+  Decision (uncurry P x y) := P_dec (x,y).
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 9781417419db2d5d44b013fdcf864fb3ebc1d1fb..35808597bc1ab411f30f29422ec9b88371ca8ad4 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -3,7 +3,7 @@
 (** This file collects definitions and theorems on finite collections. Most
 importantly, it implements a fold and size function and some useful induction
 principles on finite collections . *)
-Require Import Permutation.
+Require Import Permutation ars.
 Require Export collections numbers listset.
 
 Instance collection_size `{Elements A C} : Size C := length ∘ elements.
@@ -37,6 +37,8 @@ Proof.
 Qed.
 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_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅.
+Proof. by rewrite size_empty_iff. Qed.
 
 Lemma size_singleton (x : A) : size {[ x ]} = 1.
 Proof.
@@ -123,54 +125,38 @@ Qed.
 
 Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
 Proof.
-  rewrite <-size_union. by rewrite union_difference. solve_elem_of.
-Qed.
-Lemma size_add X x : x ∉ X → size ({[ x ]} ∪ X) = S (size X).
-Proof.
-  intros. rewrite size_union. by rewrite size_singleton. solve_elem_of.
-Qed.
-
-Lemma size_difference X Y : X ⊆ Y → size X + size (Y ∖ X) = size Y.
-Proof. intros. by rewrite <-size_union_alt, subseteq_union_1. Qed.
-Lemma size_remove X x : x ∈ X → S (size (X ∖ {[ x ]})) = size X.
-Proof.
-  intros. rewrite <-(size_difference {[ x ]} X).
-  * rewrite size_singleton. auto with arith.
-  * solve_elem_of.
+  rewrite <-size_union by solve_elem_of.
+  setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by esolve_elem_of.
+  rewrite <-union_difference, (commutative (∪)); solve_elem_of.
 Qed.
 
 Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
 Proof.
-  intros. rewrite <-(subseteq_union_1 X Y) by done.
-  rewrite <-(union_difference X Y), size_union by solve_elem_of.
-  auto with arith.
+  intros. rewrite (union_difference X Y), size_union_alt by done. lia.
 Qed.
-
-Lemma collection_wf_ind (P : C → Prop) :
-  (∀ X, (∀ Y, size Y < size X → P Y) → P X) →
-  ∀ X, P X.
+Lemma subset_size X Y : X ⊂ Y → size X < size Y.
 Proof.
-  intros Hind. cut (∀ n X, size X < n → P X).
-  { intros help X. apply help with (S (size X)). auto with arith. }
-  induction n; intros.
-  * by destruct (Lt.lt_n_0 (size X)).
-  * apply Hind. intros. apply IHn. eauto with arith.
+  intros. rewrite (union_difference X Y) by solve_elem_of.
+  rewrite size_union_alt, difference_twice.
+  cut (size (Y ∖ X) ≠ 0); [lia |].
+  by apply size_non_empty_iff, non_empty_difference.
 Qed.
 
+Lemma collection_wf : wf (@subset C _).
+Proof. apply well_founded_lt_compat with size, subset_size. Qed.
+
 Lemma collection_ind (P : C → Prop) :
   Proper ((≡) ==> iff) P →
   P ∅ →
   (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) →
   ∀ X, P X.
 Proof.
-  intros ? Hemp Hadd. apply collection_wf_ind.
-  intros X IH. destruct (Compare_dec.zerop (size X)).
-  * by rewrite size_empty_inv.
-  * destruct (size_pos_choose X); auto.
-    rewrite <-(subseteq_union_1 {[ x ]} X) by solve_elem_of.
-    rewrite <-union_difference.
-    apply Hadd; [solve_elem_of |]. apply IH.
-    rewrite <-(size_remove X x); auto with arith.
+  intros ? Hemp Hadd. apply well_founded_induction with (⊂).
+  { apply collection_wf. }
+  intros X IH. destruct (elem_of_or_empty X) as [[x ?]|HX].
+  * rewrite (union_difference {[ x ]} X) by solve_elem_of.
+    apply Hadd. solve_elem_of. apply IH. esolve_elem_of.
+  * by rewrite HX.
 Qed.
 
 Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
@@ -182,16 +168,12 @@ Proof.
   intros ? Hemp Hadd.
   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].
+  induction 1 as [|x l ?? IH]; simpl.
   * intros X HX. setoid_rewrite elem_of_nil in HX.
-    rewrite equiv_empty; firstorder.
+    rewrite equiv_empty. done. esolve_elem_of.
   * 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.
-    intros y. split.
-    + intros. destruct (proj1 (HX y)); solve_elem_of.
-    + esolve_elem_of.
+    rewrite (union_difference {[ x ]} X) by esolve_elem_of.
+    apply Hadd. solve_elem_of. apply IH. esolve_elem_of.
 Qed.
 
 Lemma collection_fold_proper {B} (R : relation B)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d767568d569c1ee5001fb20807ab487bd8826608..c6e75cb4a996822f8b7b942ad2b77359797b04b5 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -4,6 +4,7 @@
 finite maps and collects some theory on it. Most importantly, it proves useful
 induction principles for finite maps and implements the tactic [simplify_map]
 to simplify goals involving finite maps. *)
+Require Import Permutation.
 Require Export prelude.
 (** * Axiomatization of finite maps *)
 (** We require Leibniz equality to be extensional on finite maps. This of
@@ -13,17 +14,22 @@ 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. *)
+(** Finiteness is axiomatized by requiring that each map can be translated
+to an association list. The translation to association lists is used to
+implement the [dom] function, and for well founded recursion on finite maps. *)
 
 (** 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 FinMapToList K A M := finmap_to_list: M → list (K * A).
+
 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}
+    `{∀ A, Lookup K A (M A)}
+    `{∀ A, Empty (M A)}
+    `{∀ A, PartialAlter K A (M A)}
+    `{∀ A, Merge A (M A)}
+    `{∀ A, FinMapToList K A (M A)}
     `{∀ i j : K, Decision (i = j)} := {
   finmap_eq {A} (m1 m2 : M A) :
     (∀ i, m1 !! i = m2 !! i) → m1 = m2;
@@ -35,8 +41,10 @@ Class FinMap K M `{!FMap M}
     i ≠ j → partial_alter f i m !! j = m !! j;
   lookup_fmap {A B} (f : A → B) (m : M A) i :
     (f <$> m) !! i = f <$> m !! i;
-  elem_of_dom C {A} `{Collection K C} (m : M A) i :
-    i ∈ dom C m ↔ is_Some (m !! i);
+  finmap_to_list_nodup {A} (m : M A) :
+    NoDup (finmap_to_list m);
+  elem_of_finmap_to_list {A} (m : M A) i x :
+    (i,x) ∈ finmap_to_list m ↔ m !! i = Some x;
   merge_spec {A} f `{!PropHolds (f None None = None)}
     (m1 m2 : M A) i : merge f m1 m2 !! i = f (m1 !! i) (m2 !! i)
 }.
@@ -46,43 +54,48 @@ Class FinMap K M `{!FMap M}
 finite map implementations. These generic implementations do not cause a
 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,
+Instance finmap_insert `{PartialAlter K A M} : Insert K A M := λ i x,
   partial_alter (λ _, Some x) i.
-Instance finmap_alter `{PartialAlter K M A} : Alter K M A := λ f,
+Instance finmap_alter `{PartialAlter K A M} : Alter K A M := λ f,
   partial_alter (fmap f).
-Instance finmap_delete `{PartialAlter K M A} : Delete K M :=
+Instance finmap_delete `{PartialAlter K A M} : Delete K M :=
   partial_alter (λ _, None).
-
-Instance finmap_singleton `{PartialAlter K M A}
+Instance finmap_singleton `{PartialAlter K A M}
   `{Empty M} : Singleton (K * A) M := λ p, <[fst p:=snd p]>∅.
-Definition list_to_map `{Insert K M A} `{Empty M}
+
+Definition finmap_of_list `{Insert K A M} `{Empty M}
   (l : list (K * A)) : M := insert_list l ∅.
+Instance finmap_dom `{FinMapToList K A M} : Dom K M := λ C _ _ _,
+  foldr ((∪) ∘ singleton ∘ fst) ∅ ∘ finmap_to_list.
 
-Instance finmap_union_with `{Merge M} : UnionWith M := λ A f,
+Instance finmap_union_with `{Merge A M} : UnionWith A M := λ f,
   merge (union_with f).
-Instance finmap_intersection_with `{Merge M} : IntersectionWith M := λ A f,
+Instance finmap_intersection_with `{Merge A M} : IntersectionWith A M := λ f,
   merge (intersection_with f).
-Instance finmap_difference_with `{Merge M} : DifferenceWith M := λ A f,
+Instance finmap_difference_with `{Merge A M} : DifferenceWith A M := λ f,
   merge (difference_with f).
 
 (** 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).
+Definition finmap_forall `{Lookup K A M} (P : K → A → Prop) : M → Prop :=
+  λ m, ∀ i x, m !! i = Some x → P i x.
+Definition finmap_intersection_forall `{Lookup K A M}
+    (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 A (M A)} : Disjoint (M A) := λ A,
+  finmap_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_intersection `{Merge M} {A} : Intersection (M A) :=
-  union_with (λ x _, x).
+Instance finmap_union `{Merge A M} : Union M :=
+  union_with (λ x _, Some x).
+Instance finmap_intersection `{Merge A M} : Intersection M :=
+  union_with (λ x _, Some 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) :=
+Instance finmap_difference `{Merge A M} : Difference M :=
   difference_with (λ _ _, None).
 
 (** * General theorems *)
@@ -97,6 +110,9 @@ Section finmap_common.
   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_is_Some (m1 m2 : M A) i :
+    is_Some (m1 !! i) → m1 ⊆ m2 → is_Some (m2 !! i).
+  Proof. inversion 1. eauto using lookup_weaken. Qed.
   Lemma lookup_weaken_None (m1 m2 : M A) i :
     m2 !! i = None → m1 ⊆ m2 → m1 !! i = None.
   Proof.
@@ -116,26 +132,9 @@ Section finmap_common.
 
   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 inversion 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).
+  Lemma lookup_empty_is_Some 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.
@@ -272,15 +271,9 @@ Section finmap_common.
     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.
@@ -289,16 +282,6 @@ Section finmap_common.
     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.
@@ -330,6 +313,117 @@ Section finmap_common.
     rewrite IHis, delete_insert_comm; intuition.
   Qed.
 
+  Lemma elem_of_dom C `{SimpleCollection K C} (m : M A) i :
+    i ∈ dom C m ↔ is_Some (m !! i).
+  Proof.
+    unfold dom, finmap_dom. simpl. rewrite is_Some_alt.
+    setoid_rewrite <-elem_of_finmap_to_list.
+    induction (finmap_to_list m) as [|[j x] l IH]; simpl.
+    * rewrite elem_of_empty.
+      setoid_rewrite elem_of_nil. naive_solver.
+    * rewrite elem_of_union, elem_of_singleton.
+      setoid_rewrite elem_of_cons. naive_solver.
+  Qed.
+  Lemma not_elem_of_dom C `{SimpleCollection 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 dom_empty C `{SimpleCollection K C} : dom C (∅ : M A) ≡ ∅.
+  Proof.
+    split; intro.
+    * rewrite (elem_of_dom C), lookup_empty. by inversion 1.
+    * solve_elem_of.
+  Qed.
+  Lemma dom_empty_inv C `{SimpleCollection 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 delete_partial_alter_dom C `{SimpleCollection 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_dom C `{SimpleCollection 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 elem_of_dom_delete C `{SimpleCollection 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 `{SimpleCollection K C} (m : M A) i :
+    i ∉ dom C (delete i m).
+  Proof. apply (not_elem_of_dom C), lookup_delete. Qed.
+
+  Lemma subseteq_dom C `{SimpleCollection K C} (m1 m2 : M A) :
+    m1 ⊆ m2 → dom C m1 ⊆ dom C m2.
+  Proof.
+    unfold subseteq, finmap_subseteq, collection_subseteq.
+    intros ??. rewrite !(elem_of_dom C). inversion 1. eauto.
+  Qed.
+  Lemma subset_dom C `{SimpleCollection K C} (m1 m2 : M A) :
+    m1 ⊂ m2 → dom C m1 ⊂ dom C m2.
+  Proof.
+    intros [Hss1 Hss2]. split.
+    * by apply subseteq_dom.
+    * intros Hdom. destruct Hss2. intros i x Hi.
+      specialize (Hdom i). rewrite !(elem_of_dom C) in Hdom.
+      feed inversion Hdom. eauto.
+      by erewrite (Hss1 i) in Hi by eauto.
+  Qed.
+  Lemma finmap_wf : wf (@subset (M A) _).
+  Proof.
+    apply (wf_projected (⊂) (dom (listset K))).
+    * by apply (subset_dom _).
+    * by apply collection_wf.
+  Qed.
+
+  Lemma partial_alter_subseteq (m : M A) i f :
+    m !! i = None →
+    m ⊆ partial_alter f i m.
+  Proof.
+    intros Hi j x Hj. rewrite lookup_partial_alter_ne; congruence.
+  Qed.
+  Lemma partial_alter_subset (m : M A) i f :
+    m !! i = None →
+    is_Some (f (m !! i)) →
+    m ⊂ partial_alter f i m.
+  Proof.
+    intros Hi Hfi. split.
+    * by apply partial_alter_subseteq.
+    * inversion Hfi as [x Hx]. intros Hm.
+      apply (Some_ne_None x). rewrite <-(Hm i x); [done|].
+      by rewrite lookup_partial_alter.
+  Qed.
+  Lemma insert_subseteq (m : M A) i x :
+    m !! i = None →
+    m ⊆ <[i:=x]>m.
+  Proof. apply partial_alter_subseteq. Qed.
+  Lemma insert_subset (m : M A) i x :
+    m !! i = None →
+    m ⊂ <[i:=x]>m.
+  Proof. intro. apply partial_alter_subset; eauto. Qed.
+
+  Lemma delete_subseteq (m : M A) i :
+    delete i m ⊆ m.
+  Proof. intros j x. rewrite lookup_delete_Some. tauto. Qed.
+  Lemma delete_subseteq_compat (m1 m2 : M A) i :
+    m1 ⊆ m2 →
+    delete i m1 ⊆ delete i m2.
+  Proof. intros ? j x. rewrite !lookup_delete_Some. intuition eauto. Qed.
+  Lemma delete_subset_alt (m : M A) i x :
+    m !! i = Some x → delete i m ⊂ m.
+  Proof.
+    split.
+    * apply delete_subseteq.
+    * intros Hi. apply (None_ne_Some x).
+      by rewrite <-(lookup_delete m i), (Hi i x).
+  Qed.
+  Lemma delete_subset (m : M A) i :
+    is_Some (m !! i) → delete i m ⊂ m.
+  Proof. inversion 1. eauto using delete_subset_alt. Qed.
+
   (** * Induction principles *)
   (** We use the induction principle on finite collections to prove the
   following induction principle on finite maps. *)
@@ -369,49 +463,6 @@ Section finmap_common.
     setoid_rewrite <-(not_elem_of_dom (listset _)).
     apply (finmap_ind_alt (listset _) P).
   Qed.
-
-  (** * 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 *)
@@ -446,28 +497,253 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) := repeat
     feed pose proof (lookup_weaken_inv m1 m2 i x y) as H3;
       [done | by tac | done | ];
     clear H2; symmetry in H3
+  | H1 : ?m1 !! ?i = Some ?x, H2 : ?m2 !! ?i = None |- _ =>
+    let H3 := fresh in
+    assert (m1 ⊆ m2) as H3 by tac;
+    apply H3 in H1; congruence
   end.
 Tactic Notation "simplify_map_equality" := simplify_map_equality by auto.
 
+(** * More theorems on finite maps *)
 Section finmap_more.
   Context `{FinMap K M} {A : Type}.
 
-  (** * Properties on the relation [intersection_forall] *)
+  (** ** Properties of conversion to lists *)
+  Lemma finmap_to_list_unique (m : M A) i x y :
+    (i,x) ∈ finmap_to_list m →
+    (i,y) ∈ finmap_to_list m →
+    x = y.
+  Proof. rewrite !elem_of_finmap_to_list. congruence. Qed.
+  Lemma finmap_to_list_key_nodup (m : M A) :
+    NoDup (fst <$> finmap_to_list m).
+  Proof.
+    eauto using NoDup_fmap_fst, finmap_to_list_unique, finmap_to_list_nodup.
+  Qed.
+
+  Lemma elem_of_finmap_of_list_1 (l : list (K * A)) i x :
+    NoDup (fst <$> l) → (i,x) ∈ l → finmap_of_list l !! i = Some x.
+  Proof.
+    induction l as [|[j y] l IH]; simpl.
+    * by rewrite elem_of_nil.
+    * rewrite NoDup_cons, elem_of_cons, elem_of_list_fmap.
+      intros [Hl ?] [?|?]; simplify_map_equality; [done |].
+      destruct (decide (i = j)); simplify_map_equality; [| by auto].
+      destruct Hl. by exists (j,x).
+  Qed.
+  Lemma elem_of_finmap_of_list_2 (l : list (K * A)) i x :
+    finmap_of_list l !! i = Some x → (i,x) ∈ l.
+  Proof.
+    induction l as [|[j y] l IH]; simpl.
+    * by rewrite lookup_empty.
+    * rewrite elem_of_cons. destruct (decide (i = j));
+        simplify_map_equality; intuition congruence.
+  Qed.
+  Lemma elem_of_finmap_of_list (l : list (K * A)) i x :
+    NoDup (fst <$> l) →
+    (i,x) ∈ l ↔ finmap_of_list l !! i = Some x.
+  Proof.
+    split; auto using elem_of_finmap_of_list_1, elem_of_finmap_of_list_2.
+  Qed.
+
+  Lemma not_elem_of_finmap_of_list_1 (l : list (K * A)) i :
+    i ∉ fst <$> l → finmap_of_list l !! i = None.
+  Proof.
+    rewrite elem_of_list_fmap, eq_None_not_Some, is_Some_alt.
+    intros Hi [x ?]. destruct Hi. exists (i,x). simpl.
+    auto using elem_of_finmap_of_list_2.
+  Qed.
+  Lemma not_elem_of_finmap_of_list_2 (l : list (K * A)) i :
+    finmap_of_list l !! i = None → i ∉ fst <$> l.
+  Proof.
+    induction l as [|[j y] l IH]; simpl.
+    * rewrite elem_of_nil. tauto.
+    * rewrite elem_of_cons.
+      destruct (decide (i = j)); simplify_map_equality; by intuition.
+  Qed.
+  Lemma not_elem_of_finmap_of_list (l : list (K * A)) i :
+    i ∉ fst <$> l ↔ finmap_of_list l !! i = None.
+  Proof.
+    split; auto using not_elem_of_finmap_of_list_1,
+      not_elem_of_finmap_of_list_2.
+  Qed.
+
+  Lemma finmap_of_list_proper (l1 l2 : list (K * A)) :
+    NoDup (fst <$> l1) →
+    Permutation l1 l2 →
+    finmap_of_list l1 = finmap_of_list l2.
+  Proof.
+    intros ? Hperm. apply finmap_eq. intros i. apply option_eq. intros x.
+    by rewrite <-!elem_of_finmap_of_list; rewrite <-?Hperm.
+  Qed.
+  Lemma finmap_of_list_inj (l1 l2 : list (K * A)) :
+    NoDup (fst <$> l1) →
+    NoDup (fst <$> l2) →
+    finmap_of_list l1 = finmap_of_list l2 →
+    Permutation l1 l2.
+  Proof.
+    intros ?? Hl1l2.
+    apply NoDup_Permutation; auto using (NoDup_fmap_1 fst).
+    intros [i x]. by rewrite !elem_of_finmap_of_list, Hl1l2.
+  Qed.
+  Lemma finmap_of_to_list (m : M A) :
+    finmap_of_list (finmap_to_list m) = m.
+  Proof.
+    apply finmap_eq. intros i. apply option_eq. intros x.
+    by rewrite <-elem_of_finmap_of_list, elem_of_finmap_to_list
+      by auto using finmap_to_list_key_nodup.
+  Qed.
+  Lemma finmap_to_of_list (l : list (K * A)) :
+    NoDup (fst <$> l) →
+    Permutation (finmap_to_list (finmap_of_list l)) l.
+  Proof.
+    auto using finmap_of_list_inj,
+      finmap_to_list_key_nodup, finmap_of_to_list.
+  Qed.
+  Lemma finmap_to_list_inj (m1 m2 : M A) :
+    Permutation (finmap_to_list m1) (finmap_to_list m2) →
+    m1 = m2.
+  Proof.
+    intros.
+    rewrite <-(finmap_of_to_list m1), <-(finmap_of_to_list m2).
+    auto using finmap_of_list_proper, finmap_to_list_key_nodup.
+  Qed.
+
+  Lemma finmap_to_list_empty :
+    finmap_to_list ∅ = @nil (K * A).
+  Proof.
+    apply elem_of_nil_inv. intros [i x].
+    rewrite elem_of_finmap_to_list. apply lookup_empty_Some.
+  Qed.
+  Lemma finmap_to_list_insert (m : M A) i x :
+    m !! i = None →
+    Permutation (finmap_to_list (<[i:=x]>m)) ((i,x) :: finmap_to_list m).
+  Proof.
+    intros. apply finmap_of_list_inj; simpl.
+    * apply finmap_to_list_key_nodup.
+    * constructor; auto using finmap_to_list_key_nodup.
+      rewrite elem_of_list_fmap.
+      intros [[??] [? Hlookup]]; subst; simpl in *.
+      rewrite elem_of_finmap_to_list in Hlookup. congruence.
+    * by rewrite !finmap_of_to_list.
+  Qed.
+
+  Lemma finmap_of_list_nil :
+    finmap_of_list (@nil (K * A)) = ∅.
+  Proof. done. Qed.
+  Lemma finmap_of_list_cons (l : list (K * A)) i x :
+    finmap_of_list ((i, x) :: l) = <[i:=x]>(finmap_of_list l).
+  Proof. done. Qed.
+
+  Lemma finmap_to_list_empty_inv (m : M A) :
+    Permutation (finmap_to_list m) [] → m = ∅.
+  Proof. rewrite <-finmap_to_list_empty. apply finmap_to_list_inj. Qed.
+  Lemma finmap_to_list_insert_inv (m : M A) l i x :
+    Permutation (finmap_to_list m) ((i,x) :: l) →
+    m = <[i:=x]>(finmap_of_list l).
+  Proof.
+    intros Hperm. apply finmap_to_list_inj.
+    assert (NoDup (fst <$> (i, x) :: l)) as Hnodup.
+    { rewrite <-Hperm. auto using finmap_to_list_key_nodup. }
+    simpl in Hnodup. rewrite NoDup_cons in Hnodup.
+    destruct Hnodup.
+    rewrite Hperm, finmap_to_list_insert, finmap_to_of_list;
+      auto using not_elem_of_finmap_of_list_1.
+  Qed.
+
+  (** ** Properties of the forall predicate *)
+  Section finmap_forall.
+    Context (P : K → A → Prop).
+
+    Lemma finmap_forall_to_list m :
+      finmap_forall P m ↔ Forall (curry P) (finmap_to_list m).
+    Proof.
+      rewrite Forall_forall. split.
+      * intros Hforall [i x].
+        rewrite elem_of_finmap_to_list. by apply (Hforall i x).
+      * intros Hforall i x.
+        rewrite <-elem_of_finmap_to_list. by apply (Hforall (i,x)).
+    Qed.
+
+    Global Instance finmap_forall_dec
+      `{∀ i x, Decision (P i x)} m : Decision (finmap_forall P m).
+    Proof.
+      refine (cast_if (decide (Forall (curry P) (finmap_to_list m))));
+        by rewrite finmap_forall_to_list.
+    Defined.
+  End finmap_forall.
+
+  (** ** 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.
+
+    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_commutative 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_commutative. intros. by apply (commutative f).
+    Qed.
+
+    Lemma merge_associative 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_associative. intros. by apply (associative f).
+    Qed.
+
+    Lemma merge_idempotent m1 :
+      (∀ i, f (m1 !! i) (m1 !! i) = m1 !! i) →
+      merge f m1 m1 = m1.
+    Proof. intros. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed.
+    Global Instance: Idempotent (=) f → Idempotent (=) (merge f).
+    Proof.
+      intros ??. apply merge_idempotent. intros. by apply (idempotent f).
+    Qed.
+  End merge_with.
+
+  (** ** Properties on the intersection forall relation *)
   Section intersection_forall.
     Context (R : relation A).
 
-    Global Instance intersection_forall_sym:
-      Symmetric R → Symmetric (intersection_forall R).
+    Global Instance finmap_intersection_forall_sym:
+      Symmetric R → Symmetric (finmap_intersection_forall R).
     Proof. firstorder auto. Qed.
-    Lemma intersection_forall_empty_l (m : M A) : intersection_forall R ∅ m.
+    Lemma finmap_intersection_forall_empty_l (m : M A) :
+      finmap_intersection_forall R ∅ m.
     Proof. intros ???. by simpl_map. Qed.
-    Lemma intersection_forall_empty_r (m : M A) : intersection_forall R m ∅.
+    Lemma finmap_intersection_forall_empty_r (m : M A) :
+      finmap_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
+    Lemma finmap_not_intersection_forall `{∀ x y, Decision (R x y)} (m1 m2 : M A) :
+      ¬finmap_intersection_forall R m1 m2
         ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2 ∧ ¬R x1 x2.
     Proof.
       split.
@@ -494,7 +770,7 @@ Section finmap_more.
     Qed.
   End intersection_forall.
 
-  (** * Properties on the disjoint maps *)
+  (** ** Properties on the disjoint maps *)
   Lemma finmap_disjoint_alt (m1 m2 : M A) :
     m1 ⊥ m2 ↔ ∀ i, m1 !! i = None ∨ m2 !! i = None.
   Proof.
@@ -505,17 +781,17 @@ Section finmap_more.
     ¬m1 ⊥ m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2.
   Proof.
     unfold disjoint, finmap_disjoint.
-    rewrite not_intersection_forall.
-    * firstorder auto.
+    rewrite finmap_not_intersection_forall.
+    * naive_solver.
     * right. auto.
   Qed.
 
   Global Instance: Symmetric (@disjoint (M A) _).
-  Proof. apply intersection_forall_sym. auto. Qed.
+  Proof. apply finmap_intersection_forall_sym. auto. Qed.
   Lemma finmap_disjoint_empty_l (m : M A) : ∅ ⊥ m.
-  Proof. apply intersection_forall_empty_l. Qed.
+  Proof. apply finmap_intersection_forall_empty_l. Qed.
   Lemma finmap_disjoint_empty_r (m : M A) : m ⊥ ∅.
-  Proof. apply intersection_forall_empty_r. Qed.
+  Proof. apply finmap_intersection_forall_empty_r. Qed.
 
   Lemma finmap_disjoint_weaken (m1 m1' m2 m2' : M A) :
     m1' ⊥ m2' →
@@ -565,14 +841,14 @@ Section finmap_more.
     m !! i = None → m ⊥ {[(i, x)]}.
   Proof. by rewrite finmap_disjoint_singleton_r. Qed.
 
-  (** * Properties of the union and intersection operation *)
+  (** ** Properties of the union and intersection operation *)
   Section union_intersection_with.
-    Context (f : A → A → A).
+    Context (f : A → A → option 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).
+      union_with f m1 m2 !! i = f x y.
     Proof.
       intros Hx Hy. unfold union_with, finmap_union_with.
       by rewrite (merge_spec _), Hx, Hy.
@@ -593,29 +869,28 @@ Section finmap_more.
       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).
+    Global Instance: LeftId (=) ∅ (@union_with _ (M A) _ f).
     Proof. unfold union_with, finmap_union_with. apply _. Qed.
-    Global Instance: Commutative (=) f → Commutative (=) (@union_with M _ _ f).
+    Global Instance: RightId (=) ∅ (@union_with _ (M A) _ 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).
+    Global Instance:
+      Commutative (=) f → Commutative (=) (@union_with _ (M A) _ 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) _) := _.
+  Global Instance: Associative (=) (@union (M A) _).
+  Proof.
+    intros m1 m2 m3. unfold union, finmap_union, union_with, finmap_union_with.
+    apply (merge_associative _). intros i.
+    by destruct (m1 !! i), (m2 !! i), (m3 !! i).
+  Qed.
+  Global Instance: Idempotent (=) (@union (M A) _).
+    intros m. unfold union, finmap_union, union_with, finmap_union_with.
+    apply (merge_idempotent _). intros i. by destruct (m !! i).
+  Qed.
 
   Lemma finmap_union_Some_raw (m1 m2 : M A) i x :
     (m1 ∪ m2) !! i = Some x ↔
@@ -623,11 +898,15 @@ Section finmap_more.
   Proof.
     unfold union, finmap_union, union_with, finmap_union_with.
     rewrite (merge_spec _).
-    destruct (m1 !! i), (m2 !! i); compute; try intuition congruence.
+    destruct (m1 !! i), (m2 !! i); compute; 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.
+  Proof.
+    unfold union, finmap_union, union_with, finmap_union_with.
+    rewrite (merge_spec _).
+    destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
+  Qed.
 
   Lemma finmap_union_Some (m1 m2 : M A) i x :
     m1 ⊥ m2 →
@@ -652,7 +931,7 @@ Section finmap_more.
     m1 ⊥ m2 →
     m1 ∪ m2 = m2 ∪ m1.
   Proof.
-    intros Hdisjoint. apply (merge_comm (union_with (λ x _, x))).
+    intros Hdisjoint. apply (merge_commutative (union_with (λ x _, Some x))).
     intros i. specialize (Hdisjoint i).
     destruct (m1 !! i), (m2 !! i); compute; naive_solver.
   Qed.
@@ -776,7 +1055,7 @@ Section finmap_more.
   Qed.
 
   Lemma finmap_insert_list_union l (m : M A) :
-    insert_list l m = list_to_map l ∪ m.
+    insert_list l m = finmap_of_list l ∪ m.
   Proof.
     induction l; simpl.
     * by rewrite (left_id _ _).
@@ -791,7 +1070,7 @@ Section finmap_more.
     * intros. simpl_map. auto.
   Qed.
 
-  (** * Properties of the delete operation *)
+  (** ** Properties of the delete operation *)
   Lemma finmap_disjoint_delete_l (m1 m2 : M A) i :
     m1 ⊥ m2 → delete i m1 ⊥ m2.
   Proof.
@@ -844,9 +1123,9 @@ Section finmap_more.
     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.
+  (** ** Properties of the conversion from lists to maps *)
+  Lemma finmap_disjoint_of_list_l (m : M A) ixs :
+    finmap_of_list ixs ⊥ m ↔ Forall (λ ix, m !! fst ix = None) ixs.
   Proof.
     split.
     * induction ixs; simpl; rewrite ?finmap_disjoint_insert_l in *; intuition.
@@ -854,36 +1133,36 @@ Section finmap_more.
       + 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_of_list_r (m : M A) ixs :
+    m ⊥ finmap_of_list ixs ↔ Forall (λ ix, m !! fst ix = None) ixs.
+  Proof. by rewrite (symmetry_iff (⊥)), finmap_disjoint_of_list_l. Qed.
 
-  Lemma finmap_disjoint_list_to_map_zip_l (m : M A) is xs :
+  Lemma finmap_disjoint_of_list_zip_l (m : M A) is xs :
     same_length is xs →
-    list_to_map (zip is xs) ⊥ m ↔ Forall (λ i, m !! i = None) is.
+    finmap_of_list (zip is xs) ⊥ m ↔ Forall (λ i, m !! i = None) is.
   Proof.
-    intro. rewrite finmap_disjoint_list_to_map_l.
+    intro. rewrite finmap_disjoint_of_list_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 :
+  Lemma finmap_disjoint_of_list_zip_r (m : M A) is xs :
     same_length is xs →
-    m ⊥ list_to_map (zip is xs) ↔ Forall (λ i, m !! i = None) is.
+    m ⊥ finmap_of_list (zip is xs) ↔ Forall (λ i, m !! i = None) is.
   Proof.
-    intro. by rewrite (symmetry_iff (⊥)), finmap_disjoint_list_to_map_zip_l.
+    intro. by rewrite (symmetry_iff (⊥)), finmap_disjoint_of_list_zip_l.
   Qed.
-  Lemma finmap_disjoint_list_to_map_zip_l_2 (m : M A) is xs :
+  Lemma finmap_disjoint_of_list_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 :
+    finmap_of_list (zip is xs) ⊥ m.
+  Proof. intro. by rewrite finmap_disjoint_of_list_zip_l. Qed.
+  Lemma finmap_disjoint_of_list_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.
+    m ⊥ finmap_of_list (zip is xs).
+  Proof. intro. by rewrite finmap_disjoint_of_list_zip_r. Qed.
 
-  (** * Properties with respect to vectors of elements *)
+  (** ** Properties with respect to vectors *)
   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.
@@ -930,11 +1209,12 @@ Section finmap_more.
     * by apply Forall_vlookup.
   Qed.
 
-  (** * Properties of the difference operation *)
+  (** ** 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.
+    unfold difference, finmap_difference,
+      difference_with, finmap_difference_with.
     rewrite (merge_spec _).
     destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
   Qed.
@@ -943,9 +1223,11 @@ Section finmap_more.
     m2 ⊆ m3 → m1 ∖ m3 ⊥ m2.
   Proof.
     intros E i. specialize (E i).
-    unfold difference, finmap_difference, difference_with, finmap_difference_with.
+    unfold difference, finmap_difference,
+      difference_with, finmap_difference_with.
     rewrite (merge_spec _).
-    destruct (m1 !! i), (m2 !! i), (m3 !! i); compute; try intuition congruence.
+    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) :
@@ -957,17 +1239,19 @@ Section finmap_more.
   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.
+    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]
+(** * Tactic to decompose disjoint assumptions *)
+(** The tactic [decompose_map_disjoint] simplifies occurences of [disjoint]
 in the conclusion and hypotheses that involve the union, insert, or singleton
 operation. *)
-Ltac decompose_finmap_disjoint := repeat
+Ltac decompose_map_disjoint := repeat
   match goal with
   | H : _ ∪ _ ⊥ _ |- _ =>
     apply finmap_disjoint_union_l in H; destruct H
@@ -990,5 +1274,7 @@ Ltac decompose_finmap_disjoint := repeat
   | H : Forall (⊥ _) _ |- _ => rewrite Forall_vlookup in H
   | H : Forall (⊥ _) [] |- _ => clear H
   | H : Forall (⊥ _) (_ :: _) |- _ =>
-    apply Forall_inv in H; destruct H
+    rewrite Forall_cons in H; destruct H
+  | H : Forall (⊥ _) (_ :: _) |- _ =>
+    rewrite Forall_app in H; destruct H
   end.
diff --git a/theories/list.v b/theories/list.v
index 94de696a04431530e1c10dbd12e66cde63f6618f..0a5141079df66eb52f90ab7000efe52e0479a763 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2,6 +2,7 @@
 (* 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 Permutation.
 Require Export base decidable option numbers.
 
@@ -11,6 +12,9 @@ Arguments app {_} _ _.
 Arguments Permutation {_} _ _.
 Arguments Forall_cons {_} _ _ _ _ _.
 
+Notation Forall_nil_2 := Forall_nil.
+Notation Forall_cons_2 := Forall_cons.
+
 Notation tail := tl.
 Notation take := firstn.
 Notation drop := skipn.
@@ -26,8 +30,8 @@ Notation "( l ++)" := (app l) (only parsing) : C_scope.
 Notation "(++ k )" := (λ l, app l k) (only parsing) : C_scope.
 
 (** * General definitions *)
-(** Looking up elements and updating elements in a list. *)
-Instance list_lookup {A} : Lookup nat (list A) A :=
+(** Looking up, updating, and deleting elements of a list. *)
+Instance list_lookup {A} : Lookup nat A (list A) :=
   fix go (i : nat) (l : list A) {struct l} : option A :=
   match l with
   | [] => None
@@ -37,7 +41,7 @@ Instance list_lookup {A} : Lookup nat (list A) A :=
     | S i => @lookup _ _ _ go i l
     end
   end.
-Instance list_alter {A} (f : A → A) : AlterD nat (list A) A f :=
+Instance list_alter {A} (f : A → A) : AlterD nat A (list A) f :=
   fix go (i : nat) (l : list A) {struct l} :=
   match l with
   | [] => []
@@ -57,9 +61,62 @@ Instance list_delete {A} : Delete nat (list A) :=
     | S i => x :: @delete _ _ go i l
     end
   end.
-Instance list_insert {A} : Insert nat (list A) A := λ i x,
+Instance list_insert {A} : Insert nat A (list A) := λ i x,
   alter (λ _, x) i.
 
+(** 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]) [].
+
+(** The function [filter P l] returns the list of elements of [l] that
+satisfies [P]. The order remains unchanged. *)
+Instance list_filter {A} : Filter A (list A) :=
+  fix go P _ l :=
+  match l with
+  | [] => []
+  | x :: l =>
+     if decide (P x)
+     then x :: @filter _ _ (@go) _ _ l
+     else @filter _ _ (@go) _ _ l
+  end.
+
+(** The function [replicate n x] generates a list with length [n] of elements
+with value [x]. *)
+Fixpoint replicate {A} (n : nat) (x : A) : list A :=
+  match n with
+  | 0 => []
+  | S n => x :: replicate n x
+  end.
+
+(** The function [reverse l] returns the elements of [l] in reverse order. *)
+Definition reverse {A} (l : list A) : list A := rev_append l [].
+
+(** The function [resize n y l] takes the first [n] elements of [l] in case
+[length l ≤ n], and otherwise appends elements with value [x] to [l] to obtain
+a list of length [n]. *)
+Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
+  match l with
+  | [] => replicate n y
+  | x :: l =>
+    match n with
+    | 0 => []
+    | S n => x :: resize n y l
+    end
+  end.
+Arguments resize {_} !_ _ !_.
+
+(** The predicate [prefix_of] holds if the first list is a prefix of the second.
+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.
+
+(** * Tactics on lists *)
+Lemma cons_inv {A} (l1 l2 : list A) x1 x2 :
+  x1 :: l1 = x2 :: l2 → x1 = x2 ∧ l1 = l2.
+Proof. by injection 1. Qed.
+
+(** The tactic [discriminate_list_equality] discharges goals containing
+invalid list equalities as an assumption. *)
 Tactic Notation "discriminate_list_equality" hyp(H) :=
   apply (f_equal length) in H;
   repeat (simpl in H || rewrite app_length in H);
@@ -67,42 +124,41 @@ Tactic Notation "discriminate_list_equality" hyp(H) :=
 Tactic Notation "discriminate_list_equality" :=
   repeat_on_hyps (fun H => discriminate_list_equality H).
 
+(** The tactic [simplify_list_equality] simplifies assumptions involving
+equalities on lists. *)
 Ltac simplify_list_equality := repeat
   match goal with
-  | _ => progress simplify_equality
+  | H : _ :: _ = _ :: _ |- _ =>
+     apply cons_inv in H; destruct H
+     (* to circumvent bug #2939 in some situations *)
   | H : _ ++ _ = _ ++ _ |- _ => first
-     [ apply app_inv_head in H
+     [ apply app_inj_tail in H; destruct H
+     | apply app_inv_head in H
      | apply app_inv_tail in H ]
+  | H : [?x] !! ?i = Some ?y |- _ =>
+     destruct i; [change (Some x = Some y) in H|discriminate]
+  | _ => progress simplify_equality
   | 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]) [].
-
-(** The predicate [prefix_of] holds if the first list is a prefix of the second.
-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: ∀ x : A, Injective (=) (=) (x ::).
+Proof. by injection 1. Qed.
+Global Instance: ∀ l : list A, Injective (=) (=) (:: l).
+Proof. by injection 1. 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 app_inj (l1 k1 l2 k2 : list A) :
+  length l1 = length k1 →
+  l1 ++ l2 = k1 ++ k2 → l1 = k1 ∧ l2 = k2.
+Proof. revert k1. induction l1; intros [|??]; naive_solver. Qed.
+
 Lemma list_eq (l1 l2 : list A) : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
 Proof.
   revert l2. induction l1; intros [|??] H.
@@ -117,6 +173,14 @@ Proof. intros. by apply list_eq. Qed.
 
 Global Instance list_eq_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ l k,
   Decision (l = k) := list_eq_dec dec.
+Definition list_singleton_dec (l : list A) : { x | l = [x] } + { length l ≠ 1 }.
+Proof.
+ by refine (
+  match l with
+  | [x] => inleft (x ↾ _)
+  | _ => inright _
+  end).
+Defined.
 
 Lemma nil_or_length_pos (l : list A) : l = [] ∨ length l ≠ 0.
 Proof. destruct l; simpl; auto with lia. Qed.
@@ -156,6 +220,19 @@ Lemma lookup_ge_length_2 (l : list A) i :
   length l ≤ i → l !! i = None.
 Proof. by rewrite lookup_ge_length. Qed.
 
+Lemma list_eq_length_eq (l1 l2 : list A) :
+  length l2 = length l1 →
+  (∀ i x y, l1 !! i = Some x → l2 !! i = Some y → x = y) →
+  l1 = l2.
+Proof.
+  intros Hlength Hlookup. apply list_eq. intros i.
+  destruct (l2 !! i) as [x|] eqn:E.
+  * feed inversion (lookup_lt_length_2 l1 i) as [y].
+    { pose proof (lookup_lt_length_alt l2 i x E). lia. }
+    f_equal. eauto.
+  * rewrite lookup_ge_length in E |- *. lia.
+Qed.
+
 Lemma lookup_app_l (l1 l2 : list A) i :
   i < length l1 →
   (l1 ++ l2) !! i = l1 !! i.
@@ -200,26 +277,6 @@ Lemma list_lookup_middle (l1 l2 : list A) (x : A) :
   (l1 ++ x :: l2) !! length l1 = Some x.
 Proof. by induction l1; simpl. Qed.
 
-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.
-  * by destruct (le_Sn_0 j).
-  * destruct j; simpl; auto with arith.
-Qed.
-
-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.
-  * by destruct (le_Sn_0 i).
-  * simpl; auto with arith.
-Qed.
-
-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 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.
@@ -248,6 +305,17 @@ 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 list_lookup_other (l : list A) i x :
+  length l ≠ 1 →
+  l !! i = Some x →
+  ∃ j y, j ≠ i ∧ l !! j = Some y.
+Proof.
+  intros Hl Hi.
+  destruct i; destruct l as [|x0 [|x1 l]]; simpl in *; simplify_equality.
+  * by exists 1 x1.
+  * by exists 0 x0.
+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.
@@ -281,30 +349,6 @@ Lemma insert_app_r_alt (l1 l2 : list A) i x :
   <[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 !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.
-Proof take_alter _ _ _ _.
-
-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 !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 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.
@@ -315,14 +359,17 @@ 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 :
+Lemma elem_of_cons (l : list A) x y :
   x ∈ y :: l ↔ x = y ∨ x ∈ l.
 Proof.
   split.
   * inversion 1; subst. by left. by right.
   * intros [?|?]; subst. by left. by right.
 Qed.
-Lemma elem_of_app (x : A) l1 l2 :
+Lemma not_elem_of_cons (l : list A) x y :
+  x ∉ y :: l ↔ x ≠ y ∧ x ∉ l.
+Proof. rewrite elem_of_cons. tauto. Qed.
+Lemma elem_of_app (l1 l2 : list A) x :
   x ∈ l1 ++ l2 ↔ x ∈ l1 ∨ x ∈ l2.
 Proof.
   induction l1.
@@ -330,6 +377,10 @@ Proof.
     by destruct (elem_of_nil x).
   * simpl. rewrite !elem_of_cons, IHl1. tauto.
 Qed.
+Lemma not_elem_of_app (l1 l2 : list A) x :
+  x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2.
+Proof. rewrite elem_of_app. tauto. Qed.
+
 Lemma elem_of_list_singleton (x y : A) : x ∈ [y] ↔ x = y.
 Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.
 
@@ -337,7 +388,7 @@ 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 elem_of_list_split (x : A) l :
+Lemma elem_of_list_split (l : list A) x :
   x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2.
 Proof.
   induction 1 as [x l|x y l ? [l1 [l2 ?]]].
@@ -398,7 +449,7 @@ Proof.
     naive_solver.
 Qed.
 
-Global Instance NoDup_permutation_proper:
+Global Instance NoDup_proper:
   Proper (Permutation ==> iff) (@NoDup A).
 Proof.
   induction 1 as [|x l k Hlk IH | |].
@@ -416,7 +467,7 @@ Proof.
     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.
+    destruct (elem_of_list_split k x) as [l1 [l2 ?]]; subst.
     { rewrite <-Hlk. by constructor. }
     rewrite <-Permutation_middle, NoDup_cons in Hk.
     destruct Hk as [??].
@@ -466,6 +517,19 @@ Section remove_dups.
   Qed.
 End remove_dups.
 
+Lemma elem_of_list_filter `{∀ x : A, Decision (P x)} l x :
+  x ∈ filter P l ↔ P x ∧ x ∈ l.
+Proof.
+  unfold filter. induction l; simpl; repeat case_decide;
+     rewrite ?elem_of_nil, ?elem_of_cons; naive_solver.
+Qed.
+Lemma filter_nodup P `{∀ x : A, Decision (P x)} l :
+  NoDup l → NoDup (filter P l).
+Proof.
+  unfold filter. induction 1; simpl; repeat case_decide;
+    rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto.
+Qed.
+
 Lemma reverse_nil : reverse [] = @nil A.
 Proof. done. Qed.
 Lemma reverse_cons (l : list A) x : reverse (x :: l) = reverse l ++ [x].
@@ -480,6 +544,113 @@ 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 take_nil n :
+  take n (@nil A) = [].
+Proof. by destruct n. Qed.
+Lemma take_app (l k : list A) :
+  take (length l) (l ++ k) = l.
+Proof. induction l; simpl; f_equal; auto. Qed.
+Lemma take_app_alt (l k : list A) n :
+  n = length l →
+  take n (l ++ k) = l.
+Proof. intros Hn. by rewrite Hn, take_app. Qed.
+Lemma take_app_le (l k : list A) n :
+  n ≤ length l →
+  take n (l ++ k) = take n l.
+Proof.
+  revert n;
+  induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
+Qed.
+Lemma take_app_ge (l k : list A) n :
+  length l ≤ n →
+  take n (l ++ k) = l ++ take (n - length l) k.
+Proof.
+  revert n;
+  induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
+Qed.
+Lemma take_ge (l : list A) n :
+  length l ≤ n →
+  take n l = l.
+Proof.
+  revert n.
+  induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
+Qed.
+
+Lemma take_take (l : list A) n m :
+  take n (take m l) = take (min n m) l.
+Proof. revert n m. induction l; intros [|?] [|?]; simpl; f_equal; auto. Qed.
+Lemma take_idempotent (l : list A) n :
+  take n (take n l) = take n l.
+Proof. by rewrite take_take, Min.min_idempotent. Qed.
+
+Lemma take_length (l : list A) n :
+  length (take n l) = min n (length l).
+Proof. revert n. induction l; intros [|?]; simpl; f_equal; done. Qed.
+Lemma take_length_alt (l : list A) n :
+  n ≤ length l →
+  length (take n l) = n.
+Proof. rewrite take_length. apply Min.min_l. Qed.
+
+Lemma lookup_take (l : list A) n i :
+  i < n → take n l !! i = l !! i.
+Proof.
+  revert n i. induction l; intros [|n] i ?; trivial.
+  * auto with lia.
+  * destruct i; simpl; auto with arith.
+Qed.
+Lemma lookup_take_ge (l : list A) n i :
+  n ≤ i → take n l !! i = None.
+Proof.
+  revert n i.
+  induction l; intros [|?] [|?] ?; simpl; auto with lia.
+Qed.
+Lemma take_alter (f : A → A) l n i :
+  n ≤ i → take n (alter f i l) = take n l.
+Proof.
+  intros. apply list_eq. intros j. destruct (le_lt_dec n j).
+  * by rewrite !lookup_take_ge.
+  * by rewrite !lookup_take, !list_lookup_alter_ne by lia.
+Qed.
+Lemma take_insert (l : list A) n i x :
+  n ≤ i → take n (<[i:=x]>l) = take n l.
+Proof take_alter _ _ _ _.
+
+Lemma drop_nil n :
+  drop n (@nil A) = [].
+Proof. by destruct n. Qed.
+Lemma drop_app (l k : list A) :
+  drop (length l) (l ++ k) = k.
+Proof. induction l; simpl; f_equal; auto. Qed.
+Lemma drop_app_alt (l k : list A) n :
+  n = length l →
+  drop n (l ++ k) = k.
+Proof. intros Hn. by rewrite Hn, drop_app. Qed.
+Lemma drop_length (l : list A) n :
+  length (drop n l) = length l - n.
+Proof.
+  revert n. by induction l; intros [|i]; simpl; f_equal.
+Qed.
+Lemma drop_all (l : list A) :
+  drop (length l) l = [].
+Proof. induction l; simpl; auto. Qed.
+Lemma drop_all_alt (l : list A) n :
+  n = length l →
+  drop n l = [].
+Proof. intros. subst. by rewrite drop_all. Qed.
+
+Lemma lookup_drop (l : list A) n i :
+  drop n l !! i = l !! (n + i).
+Proof. revert n i. induction l; intros [|i] ?; simpl; auto. Qed.
+Lemma drop_alter (f : A → A) l n i  :
+  i < n → drop n (alter f i l) = drop n l.
+Proof.
+  intros. apply list_eq. intros j.
+  by rewrite !lookup_drop, !list_lookup_alter_ne by lia.
+Qed.
+Lemma drop_insert (l : list A) n i x :
+  i < n → drop n (<[i:=x]>l) = drop n l.
+Proof drop_alter _ _ _ _.
+
 Lemma replicate_length n (x : A) : length (replicate n x) = n.
 Proof. induction n; simpl; auto. Qed.
 Lemma lookup_replicate n (x : A) i :
@@ -495,6 +666,155 @@ Proof.
   revert i.
   induction n; intros [|?]; naive_solver auto with lia.
 Qed.
+Lemma replicate_plus n m (x : A) :
+  replicate (n + m) x = replicate n x ++ replicate m x.
+Proof. induction n; simpl; f_equal; auto. Qed.
+
+Lemma take_replicate n m (x : A) :
+  take n (replicate m x) = replicate (min n m) x.
+Proof. revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
+Lemma take_replicate_plus n m (x : A) :
+  take n (replicate (n + m) x) = replicate n x.
+Proof. by rewrite take_replicate, min_l by lia. Qed.
+Lemma drop_replicate n m (x : A) :
+  drop n (replicate m x) = replicate (m - n) x.
+Proof. revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
+Lemma drop_replicate_plus n m (x : A) :
+  drop n (replicate (n + m) x) = replicate m x.
+Proof. rewrite drop_replicate. f_equal. lia. Qed.
+
+Lemma resize_spec (l : list A) n x :
+  resize n x l = take n l ++ replicate (n - length l) x.
+Proof.
+  revert n.
+  induction l; intros [|?]; simpl; f_equal; auto.
+Qed.
+Lemma resize_0 (l : list A) x :
+  resize 0 x l = [].
+Proof. by destruct l. Qed.
+Lemma resize_nil n (x : A) :
+  resize n x [] = replicate n x.
+Proof. rewrite resize_spec. rewrite take_nil. simpl. f_equal. lia. Qed.
+Lemma resize_ge (l : list A) n x :
+  length l ≤ n →
+  resize n x l = l ++ replicate (n - length l) x.
+Proof. intros. by rewrite resize_spec, take_ge. Qed.
+Lemma resize_le (l : list A) n x :
+  n ≤ length l →
+  resize n x l = take n l.
+Proof.
+  intros. rewrite resize_spec, (proj2 (NPeano.Nat.sub_0_le _ _)) by done.
+  simpl. by rewrite app_nil_r.
+Qed.
+
+Lemma resize_all (l : list A) x :
+  resize (length l) x l = l.
+Proof. intros. by rewrite resize_le, take_ge. Qed.
+Lemma resize_all_alt (l : list A) n x :
+  n = length l →
+  resize n x l = l.
+Proof. intros. subst. by rewrite resize_all. Qed.
+
+Lemma resize_plus (l : list A) n m x :
+  resize (n + m) x l = resize n x l ++ resize m x (drop n l).
+Proof.
+  revert n m.
+  induction l; intros [|?] [|?]; simpl; f_equal; auto.
+  * by rewrite plus_0_r, app_nil_r.
+  * by rewrite replicate_plus.
+Qed.
+Lemma resize_plus_eq (l : list A) n m x :
+  length l = n →
+  resize (n + m) x l = l ++ replicate m x.
+Proof.
+  intros. subst.
+  by rewrite resize_plus, resize_all, drop_all, resize_nil.
+Qed.
+
+Lemma resize_app_le (l1 l2 : list A) n x :
+  n ≤ length l1 →
+  resize n x (l1 ++ l2) = resize n x l1.
+Proof.
+  intros.
+  by rewrite !resize_le, take_app_le by (rewrite ?app_length; lia).
+Qed.
+Lemma resize_app_ge (l1 l2 : list A) n x :
+  length l1 ≤ n →
+  resize n x (l1 ++ l2) = l1 ++ resize (n - length l1) x l2.
+Proof.
+  intros.
+  rewrite !resize_spec, take_app_ge, app_assoc by done.
+  do 2 f_equal. rewrite app_length. lia.
+Qed.
+
+Lemma resize_length (l : list A) n x : length (resize n x l) = n.
+Proof.
+  rewrite resize_spec, app_length, replicate_length, take_length. lia.
+Qed.
+Lemma resize_replicate (x : A) n m :
+  resize n x (replicate m x) = replicate n x.
+Proof. revert m. induction n; intros [|?]; simpl; f_equal; auto. Qed.
+
+Lemma resize_resize (l : list A) n m x :
+  n ≤ m →
+  resize n x (resize m x l) = resize n x l.
+Proof.
+  revert n m. induction l; simpl.
+  * intros. by rewrite !resize_nil, resize_replicate.
+  * intros [|?] [|?] ?; simpl; f_equal; auto with lia.
+Qed.
+Lemma resize_idempotent (l : list A) n x :
+  resize n x (resize n x l) = resize n x l.
+Proof. by rewrite resize_resize. Qed.
+
+Lemma resize_take_le (l : list A) n m x :
+  n ≤ m →
+  resize n x (take m l) = resize n x l.
+Proof.
+  revert n m.
+  induction l; intros [|?] [|?] ?; simpl; f_equal; auto with lia.
+Qed.
+Lemma resize_take_eq (l : list A) n x :
+  resize n x (take n l) = resize n x l.
+Proof. by rewrite resize_take_le. Qed.
+
+Lemma take_resize (l : list A) n m x :
+  take n (resize m x l) = resize (min n m) x l.
+Proof.
+  revert n m.
+  induction l; intros [|?] [|?]; simpl; f_equal; auto using take_replicate.
+Qed.
+Lemma take_resize_le (l : list A) n m x :
+  n ≤ m →
+  take n (resize m x l) = resize n x l.
+Proof. intros. by rewrite take_resize, Min.min_l. Qed.
+Lemma take_resize_eq (l : list A) n x :
+  take n (resize n x l) = resize n x l.
+Proof. intros. by rewrite take_resize, Min.min_l. Qed.
+Lemma take_length_resize (l : list A) n x :
+  length l ≤ n →
+  take (length l) (resize n x l) = l.
+Proof. intros. by rewrite take_resize_le, resize_all. Qed.
+Lemma take_length_resize_alt (l : list A) n m x :
+  m = length l →
+  m ≤ n →
+  take m (resize n x l) = l.
+Proof. intros. subst. by apply take_length_resize. Qed.
+Lemma take_resize_plus (l : list A) n m x :
+  take n (resize (n + m) x l) = resize n x l.
+Proof. by rewrite take_resize, min_l by lia. Qed.
+
+Lemma drop_resize_le (l : list A) n m x :
+  n ≤ m →
+  drop n (resize m x l) = resize (m - n) x (drop n l).
+Proof.
+  revert n m. induction l; simpl.
+  * intros. by rewrite drop_nil, !resize_nil, drop_replicate.
+  * intros [|?] [|?] ?; simpl; try case_match; auto with lia.
+Qed.
+Lemma drop_resize_plus (l : list A) n m x :
+  drop n (resize (n + m) x l) = resize m x (drop n l).
+Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed.
 
 Section Forall_Exists.
   Context (P : A → Prop).
@@ -508,13 +828,15 @@ Section Forall_Exists.
       + 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_nil : Forall P [] ↔ True.
+  Proof. done. Qed.
+  Lemma Forall_cons_1 x l : Forall P (x :: l) → P x ∧ Forall P l.
+  Proof. by inversion 1. Qed.
+  Lemma Forall_cons x l : Forall P (x :: l) ↔ P x ∧ Forall P l.
+  Proof. split. by inversion 1. intros [??]. by constructor. Qed.
+  Lemma Forall_singleton x : Forall P [x] ↔ P x.
+  Proof. rewrite Forall_cons, Forall_nil; tauto. Qed.
   Lemma Forall_app l1 l2 : Forall P (l1 ++ l2) ↔ Forall P l1 ∧ Forall P l2.
   Proof.
     split.
@@ -526,6 +848,7 @@ Section Forall_Exists.
   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.
@@ -538,6 +861,9 @@ Section Forall_Exists.
     setoid_rewrite elem_of_list_lookup.
     naive_solver.
   Qed.
+  Lemma Forall_lookup_1 l i x :
+    Forall P l → l !! i = Some x → P x.
+  Proof. rewrite Forall_lookup. eauto. Qed.
   Lemma Forall_alter f l i :
     Forall P l →
     (∀ x, l !! i = Some x → P x → P (f x)) →
@@ -547,6 +873,13 @@ Section Forall_Exists.
     induction Hl; simpl; intros [|i]; constructor; auto.
   Qed.
 
+  Lemma Forall_replicate n x :
+    P x → Forall P (replicate n x).
+  Proof. induction n; simpl; constructor; auto. Qed.
+  Lemma Forall_replicate_eq n (x : A) :
+    Forall (=x) (replicate n x).
+  Proof. induction n; simpl; constructor; auto. Qed.
+
   Lemma Exists_exists l :
     Exists P l ↔ ∃ x, x ∈ l ∧ P x.
   Proof.
@@ -612,16 +945,47 @@ Section Forall_Exists.
     | right H => right (Forall_not_Exists _ H)
     end.
 End Forall_Exists.
+End general_properties.
 
 Section Forall2.
-  Context {B} (P : A → B → Prop).
+  Context {A B} (P : A → B → Prop).
+
+  Lemma Forall2_nil_inv_l k :
+    Forall2 P [] k → k = [].
+  Proof. by inversion 1. Qed.
+  Lemma Forall2_nil_inv_r k :
+    Forall2 P k [] → k = [].
+  Proof. by inversion 1. Qed.
+
+  Lemma Forall2_cons_inv l1 l2 x1 x2 :
+    Forall2 P (x1 :: l1) (x2 :: l2) → P x1 x2 ∧ Forall2 P l1 l2.
+  Proof. by inversion 1. Qed.
+  Lemma Forall2_cons_inv_l l1 k x1 :
+    Forall2 P (x1 :: l1) k → ∃ x2 l2,
+      P x1 x2 ∧ Forall2 P l1 l2 ∧ k = x2 :: l2.
+  Proof. inversion 1; subst; eauto. Qed.
+  Lemma Forall2_cons_inv_r k l2 x2 :
+    Forall2 P k (x2 :: l2) → ∃ x1 l1,
+      P x1 x2 ∧ Forall2 P l1 l2 ∧ k = x1 :: l1.
+  Proof. inversion 1; subst; eauto. Qed.
+  Lemma Forall2_cons_nil_inv l1 x1 :
+    Forall2 P (x1 :: l1) [] → False.
+  Proof. by inversion 1. Qed.
+  Lemma Forall2_nil_cons_inv l2 x2 :
+    Forall2 P [] (x2 :: l2) → False.
+  Proof. by inversion 1. Qed.
+
+  Lemma Forall2_flip l1 l2 :
+    Forall2 P l1 l2 ↔ Forall2 (flip P) l2 l1.
+  Proof. split; induction 1; constructor; auto. Qed.
 
   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.
+  Proof. intros H ?. induction H; auto. Defined.
 
   Lemma Forall2_unique l k1 k2 :
     Forall2 P l k1 →
@@ -633,32 +997,182 @@ Section Forall2.
     induction H; inversion_clear 1; intros; f_equal; eauto.
   Qed.
 
-  Lemma Forall2_Forall_1 (Q : A → Prop) l k :
+  Lemma Forall2_Forall_l (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 :
+  Proof. induction 1; inversion_clear 1; eauto. Qed.
+  Lemma Forall2_Forall_r (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.
+  Proof. induction 1; inversion_clear 1; eauto. Qed.
+
+  Lemma Forall2_lookup l1 l2 i x y :
+    Forall2 P l1 l2 →
+      l1 !! i = Some x → l2 !! i = Some y → P x y.
+  Proof.
+    intros H. revert i. induction H.
+    * discriminate.
+    * intros [|?] ??; simpl in *; simplify_equality; eauto.
+  Qed.
+  Lemma Forall2_lookup_l l1 l2 i x :
+    Forall2 P l1 l2 → l1 !! i = Some x → ∃ y,
+      l2 !! i = Some y ∧ P x y.
+  Proof.
+    intros H. revert i. induction H.
+    * discriminate.
+    * intros [|?] ?; simpl in *; simplify_equality; eauto.
+  Qed.
+  Lemma Forall2_lookup_r l1 l2 i y :
+    Forall2 P l1 l2 → l2 !! i = Some y → ∃ x,
+      l1 !! i = Some x ∧ P x y.
+  Proof.
+    intros H. revert i. induction H.
+    * discriminate.
+    * intros [|?] ?; simpl in *; simplify_equality; eauto.
+  Qed.
+
+  Lemma Forall2_alter_l f l1 l2 i :
+    Forall2 P l1 l2 →
+    (∀ x1 x2,
+      l1 !! i = Some x1 → l2 !! i = Some x2 → P x1 x2 → P (f x1) x2) →
+    Forall2 P (alter f i l1) l2.
+  Proof.
+    intros Hl. revert i.
+    induction Hl; simpl; intros [|i]; constructor; auto.
+  Qed.
+  Lemma Forall2_alter_r f l1 l2 i :
+    Forall2 P l1 l2 →
+    (∀ x1 x2,
+      l1 !! i = Some x1 → l2 !! i = Some x2 → P x1 x2 → P x1 (f x2)) →
+    Forall2 P l1 (alter f i l2).
+  Proof.
+    intros Hl. revert i.
+    induction Hl; simpl; intros [|i]; constructor; auto.
+  Qed.
+  Lemma Forall2_alter f g l1 l2 i :
+    Forall2 P l1 l2 →
+    (∀ x1 x2,
+      l1 !! i = Some x1 → l2 !! i = Some x2 → P x1 x2 → P (f x1) (g x2)) →
+    Forall2 P (alter f i l1) (alter g i l2).
+  Proof.
+    intros Hl. revert i.
+    induction Hl; simpl; intros [|i]; constructor; auto.
+  Qed.
+
+  Lemma Forall2_replicate_l l n x :
+    Forall (P x) l →
+    length l = n →
+    Forall2 P (replicate n x) l.
+  Proof.
+    intros Hl. revert n.
+    induction Hl; intros [|?] ?; simplify_equality; constructor; auto.
+  Qed.
+  Lemma Forall2_replicate_r l n x :
+    Forall (flip P x) l →
+    length l = n →
+    Forall2 P l (replicate n x).
+  Proof.
+    intros Hl. revert n.
+    induction Hl; intros [|?] ?; simplify_equality; constructor; auto.
+  Qed.
+  Lemma Forall2_replicate n x1 x2 :
+    P x1 x2 →
+    Forall2 P (replicate n x1) (replicate n x2).
+  Proof. induction n; simpl; constructor; auto. Qed.
+
+  Lemma Forall2_take l1 l2 n :
+    Forall2 P l1 l2 →
+    Forall2 P (take n l1) (take n l2).
+  Proof.
+    intros Hl1l2. revert n.
+    induction Hl1l2; intros [|?]; simpl; auto.
+  Qed.
+  Lemma Forall2_drop l1 l2 n :
+    Forall2 P l1 l2 →
+    Forall2 P (drop n l1) (drop n l2).
+  Proof.
+    intros Hl1l2. revert n.
+    induction Hl1l2; intros [|?]; simpl; auto.
+  Qed.
+  Lemma Forall2_resize l1 l2 x1 x2 n :
+    P x1 x2 →
+    Forall2 P l1 l2 →
+    Forall2 P (resize n x1 l1) (resize n x2 l2).
+  Proof.
+    intros. rewrite !resize_spec, (Forall2_length l1 l2) by done.
+    auto using Forall2_app, Forall2_take, Forall2_replicate.
+  Qed.
+
+  Lemma Forall2_resize_ge_l l1 l2 x1 x2 n m :
+    (∀ x, P x x2) →
+    n ≤ m →
+    Forall2 P (resize n x1 l1) l2 →
+    Forall2 P (resize m x1 l1) (resize m x2 l2).
+  Proof.
+    intros. assert (n = length l2).
+    { by rewrite <-(Forall2_length (resize n x1 l1) l2), resize_length. }
+    rewrite (le_plus_minus n m) by done. subst.
+    rewrite !resize_plus, resize_all, drop_all, resize_nil.
+    apply Forall2_app; [done |].
+    apply Forall2_replicate_r; [| by rewrite resize_length].
+    by apply Forall_true.
+  Qed.
+  Lemma Forall2_resize_ge_r l1 l2 x1 x2 n m :
+    (∀ x3, P x1 x3) →
+    n ≤ m →
+    Forall2 P l1 (resize n x2 l2) →
+    Forall2 P (resize m x1 l1) (resize m x2 l2).
+  Proof.
+    intros. assert (n = length l1).
+    { by rewrite (Forall2_length l1 (resize n x2 l2)), resize_length. }
+    rewrite (le_plus_minus n m) by done. subst.
+    rewrite !resize_plus, resize_all, drop_all, resize_nil.
+    apply Forall2_app; [done |].
+    apply Forall2_replicate_l; [| by rewrite resize_length].
+    by apply Forall_true.
+  Qed.
+
+  Lemma Forall2_trans {C} (Q : B → C → Prop) (R : A → C → Prop) l1 l2 l3 :
+    (∀ x1 x2 x3, P x1 x2 → Q x2 x3 → R x1 x3) →
+    Forall2 P l1 l2 →
+    Forall2 Q l2 l3 →
+    Forall2 R l1 l3.
+  Proof.
+    intros ? Hl1l2. revert l3.
+    induction Hl1l2; inversion_clear 1; eauto.
+  Qed.
+
+  Lemma Forall2_Forall (Q : A → A → Prop) l :
+    Forall (λ x, Q x x) l → Forall2 Q l l.
+  Proof. induction 1; constructor; auto. Qed.
+
+  Global Instance Forall2_dec `{∀ x1 x2, Decision (P x1 x2)} :
+    ∀ l1 l2, Decision (Forall2 P l1 l2).
+  Proof.
+   refine (
+    fix go l1 l2 : Decision (Forall2 P l1 l2) :=
+    match l1, l2 with
+    | [], [] => left _
+    | x1 :: l1, x2 :: l2 => cast_if_and (decide (P x1 x2)) (go l1 l2)
+    | _, _ => right _
+    end); clear go; abstract first [by constructor | by inversion 1].
+  Defined.
 End Forall2.
 
 Section Forall2_order.
-  Context  (R : relation A).
+  Context  {A} (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.
+    * intros ???. apply Forall2_trans. apply transitivity.
   Qed.
+  Global Instance: AntiSymmetric R → AntiSymmetric (Forall2 R).
+  Proof. induction 2; inversion_clear 1; f_equal; auto. Qed.
 End Forall2_order.
-End general_properties.
 
 Ltac decompose_elem_of_list := repeat
   match goal with
@@ -669,8 +1183,19 @@ Ltac decompose_elem_of_list := repeat
 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
+  | H : Forall _ (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
+  | H : Forall _ (_ ++ _) |- _ => rewrite Forall_app in H; destruct H
+  | H : Forall2 _ [] [] |- _ => clear H
+  | H : Forall2 _ (_ :: _) [] |- _ => destruct (Forall2_cons_nil_inv _ _ _ H)
+  | H : Forall2 _ [] (_ :: _) |- _ => destruct (Forall2_nil_cons_inv _ _ _ H)
+  | H : Forall2 _ [] ?l |- _ => apply Forall2_nil_inv_l in H; subst l
+  | H : Forall2 _ ?l [] |- _ => apply Forall2_nil_inv_r in H; subst l
+  | H : Forall2 _ (_ :: _) (_ :: _) |- _ =>
+     apply Forall2_cons_inv in H; destruct H
+  | H : Forall2 _ (_ :: _) ?l |- _ =>
+     apply Forall2_cons_inv_l in H; destruct H as (? & ? & ? & ? & ?); subst l
+  | H : Forall2 _ ?l (_ :: _) |- _ =>
+     apply Forall2_cons_inv_r in H; destruct H as (? & ? & ? & ? & ?); subst l
   end.
 
 (** * Theorems on the prefix and suffix predicates *)
@@ -889,7 +1414,12 @@ Instance list_bind {A B} (f : A → list B) : MBindD list f :=
   | [] => []
   | x :: l => f x ++ @mbind _ _ _ f go l
   end.
-Instance list_join: MJoin list := λ A, mbind id.
+Instance list_join: MJoin list :=
+  fix go A (ls : list (list A)) : list A :=
+  match ls with
+  | [] => []
+  | l :: ls => l ++ @mjoin _ go _ ls
+  end.
 
 Definition mapM `{!MBind M} `{!MRet M} {A B}
     (f : A → M B) : list A → M (list B) :=
@@ -902,12 +1432,26 @@ Definition mapM `{!MBind M} `{!MRet M} {A B}
 Section list_fmap.
   Context {A B : Type} (f : A → B).
 
+  Lemma list_fmap_compose {C} (g : B → C) l :
+    g ∘ f <$> l = g <$> f <$> l.
+  Proof. induction l; simpl; f_equal; auto. Qed.
+
+  Lemma list_fmap_ext (g : A → B) (l : list A) :
+    (∀ x, f x = g x) → fmap f l = fmap g l.
+  Proof. intro. induction l; simpl; f_equal; auto. Qed.
+  Lemma list_fmap_ext_alt (g : A → B) (l : list A) :
+    Forall (λ x, f x = g x) l ↔ fmap f l = fmap g l.
+  Proof.
+    split.
+    * induction 1; simpl; f_equal; auto.
+    * induction l; simpl; constructor; simplify_equality; auto.
+  Qed.
+
   Global Instance: Injective (=) (=) f → Injective (=) (=) (fmap f).
   Proof.
     intros ? l1. induction l1 as [|x l1 IH].
     * by intros [|??].
-    * intros [|??]; [done |]; simpl; intros; simplify_equality.
-      by f_equal; [apply (injective f) | auto].
+    * intros [|??]; simpl; intros; f_equal; simplify_equality; auto.
   Qed.
   Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
   Proof. induction l1; simpl; by f_equal. Qed.
@@ -915,7 +1459,8 @@ Section list_fmap.
     f <$> l = y :: k → ∃ x l', y = f x ∧ l = x :: l'.
   Proof. intros. destruct l; simpl; simplify_equality; eauto. Qed.
   Lemma fmap_app_inv l k1 k2 :
-    f <$> l = k1 ++ k2 → ∃ l1 l2, k1 = f <$> l1 ∧ k2 = f <$> l2 ∧ l = l1 ++ l2.
+    f <$> l = k1 ++ k2 → ∃ l1 l2,
+      k1 = f <$> l1 ∧ k2 = f <$> l2 ∧ l = l1 ++ l2.
   Proof.
     revert l. induction k1 as [|y k1 IH]; simpl.
     * intros l ?. by eexists [], l.
@@ -931,9 +1476,19 @@ Section list_fmap.
     induction l; simpl; [done |].
     by rewrite !reverse_cons, fmap_app, IHl.
   Qed.
+  Lemma fmap_replicate n x :
+    f <$> replicate n x = replicate n (f x).
+  Proof. induction n; simpl; f_equal; auto. Qed.
 
   Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
   Proof. revert i. induction l; by intros [|]. Qed.
+  Lemma list_lookup_fmap_inv l i x :
+    (f <$> l) !! i = Some x → ∃ y, x = f y ∧ l !! i = Some y.
+  Proof.
+    intros Hi. rewrite list_lookup_fmap in Hi.
+    destruct (l !! i) eqn:?; simplify_equality; eauto.
+  Qed.
+   
   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).
@@ -952,23 +1507,65 @@ Section list_fmap.
     + 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.
+  Proof.
+    firstorder eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
+  Qed.
+
+  Lemma NoDup_fmap_1 (l : list A) :
+    NoDup (f <$> l) → NoDup l.
+  Proof.
+    induction l; simpl; inversion_clear 1; constructor; auto.
+    rewrite elem_of_list_fmap in *. naive_solver.
+  Qed.
+  Lemma NoDup_fmap_2 `{!Injective (=) (=) f} (l : list A) :
+    NoDup l → NoDup (f <$> l).
+  Proof.
+    induction 1; simpl; constructor; trivial.
+    rewrite elem_of_list_fmap. intros [y [Hxy ?]].
+    apply (injective f) in Hxy. by subst.
+  Qed.
+  Lemma NoDup_fmap `{!Injective (=) (=) f} (l : list A) :
+    NoDup (f <$> l) ↔ NoDup l.
+  Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
+
+  Global Instance fmap_Permutation_proper:
+    Proper (Permutation ==> Permutation) (fmap f).
+  Proof. induction 1; simpl; econstructor; eauto. 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.
+    split; induction l; inversion_clear 1; constructor; auto.
   Qed.
 
-  Lemma mapM_fmap (g : B → option A) (l : list A) :
-    (∀ x, g (f x) = Some x) →
-    mapM g (f <$> l) = Some l.
+  Lemma Forall2_fmap_l {C} (P : B → C → Prop) l1 l2 :
+    Forall2 P (f <$> l1) l2 ↔ Forall2 (P ∘ f) l1 l2.
   Proof.
-    intros E. induction l; simpl.
-    * done.
-    * by rewrite E, IHl.
+    split; revert l2; induction l1; inversion_clear 1; constructor; auto.
   Qed.
-  Lemma mapM_fmap_inv (g : B → option A) (l : list A) (k : list B) :
+  Lemma Forall2_fmap_r {C} (P : C → B → Prop) l1 l2 :
+    Forall2 P l1 (f <$> l2) ↔ Forall2 (λ x, P x ∘ f) l1 l2.
+  Proof.
+    split; revert l1; induction l2; inversion_clear 1; constructor; auto.
+  Qed.
+  Lemma Forall2_fmap_1 {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
+    Forall2 P (f <$> l1) (g <$> l2) →
+    Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2.
+  Proof. revert l2; induction l1; intros [|??]; inversion_clear 1; auto. Qed.
+  Lemma Forall2_fmap_2 {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
+    Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2 →
+    Forall2 P (f <$> l1) (g <$> l2).
+  Proof. induction 1; simpl; auto. Qed.
+  Lemma Forall2_fmap {C D} (g : C → D) (P : B → D → Prop) l1 l2 :
+    Forall2 P (f <$> l1) (g <$> l2) ↔
+    Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2.
+  Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.
+
+  Lemma mapM_fmap_Some (g : B → option A) (l : list A) :
+    (∀ x, g (f x) = Some x) →
+    mapM g (f <$> l) = Some l.
+  Proof. intros. by induction l; simpl; simplify_option_equality. Qed.
+  Lemma mapM_fmap_Some_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.
@@ -976,8 +1573,36 @@ Section list_fmap.
     intros Hgf. revert l; induction k as [|y k]; intros [|x l] ?;
       simplify_option_equality; f_equiv; eauto.
   Qed.
+
+  Lemma mapM_Some (g : B → option A) l k :
+    Forall2 (λ x y, g x = Some y) l k →
+    mapM g l = Some k.
+  Proof. by induction 1; simplify_option_equality. Qed.
+
+  Lemma Forall2_impl_mapM (P : B → A → Prop) (g : B → option A) l k :
+    Forall (λ x, ∀ y, g x = Some y → P x y) l →
+    mapM g l = Some k →
+    Forall2 P l k.
+  Proof.
+    intros Hl. revert k. induction Hl; intros [|??] ?;
+      simplify_option_equality; eauto.
+  Qed.
 End list_fmap.
 
+Lemma NoDup_fmap_fst {A B} (l : list (A * B)) :
+  (∀ x y1 y2, (x,y1) ∈ l → (x,y2) ∈ l → y1 = y2) →
+  NoDup l →
+  NoDup (fst <$> l).
+Proof.
+  intros Hunique.
+  induction 1 as [|[x1 y1] l Hin Hnodup IH]; simpl; constructor.
+  * rewrite elem_of_list_fmap.
+    intros [[x2 y2] [??]]; simpl in *; subst. destruct Hin.
+    rewrite (Hunique x2 y1 y2); rewrite ?elem_of_cons; auto.
+  * apply IH. intros.
+    eapply Hunique; rewrite ?elem_of_cons; eauto.
+Qed.
+
 Section list_bind.
   Context {A B : Type} (f : A → list B).
 
@@ -998,38 +1623,44 @@ Section list_bind.
     * intros [y [Hx Hy]].
       induction Hy; simpl; rewrite elem_of_app; intuition.
   Qed.
+
+  Lemma Forall2_bind {C D} (g : C → list D) (P : B → D → Prop) l1 l2 :
+    Forall2 (λ x1 x2, Forall2 P (f x1) (g x2)) l1 l2 →
+    Forall2 P (l1 ≫= f) (l2 ≫= g).
+  Proof. induction 1; simpl; auto using Forall2_app. Qed.
 End list_bind.
 
 Section list_ret_join.
   Context {A : Type}.
 
+  Lemma list_join_bind (ls : list (list A)) :
+    mjoin ls = ls ≫= id.
+  Proof. induction ls; simpl; f_equal; auto. Qed.
+
   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 elem_of_list_join (x : A) (ls : list (list A)) :
+    x ∈ mjoin ls ↔ ∃ l, x ∈ l ∧ l ∈ ls.
+  Proof. by rewrite list_join_bind, elem_of_list_bind. Qed.
 
   Lemma join_nil (ls : list (list A)) :
-    mjoin ls = [] ↔ Forall (= nil) ls.
+    mjoin ls = [] ↔ Forall (= []) ls.
   Proof.
-    unfold mjoin, list_join. split.
+    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.
+    mjoin ls = [] → Forall (= []) ls.
   Proof. by rewrite join_nil. Qed.
   Lemma join_nil_2 (ls : list (list A)) :
-    Forall (= nil) ls → mjoin ls = [].
+    Forall (= []) 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.
+  Proof. 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.
@@ -1040,7 +1671,7 @@ Section list_ret_join.
     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.
+    intros Hn Hls. revert i.
     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.
@@ -1059,7 +1690,7 @@ Section list_ret_join.
     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.
+    intros Hn Hls. revert i.
     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.
@@ -1076,6 +1707,11 @@ Section list_ret_join.
     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.
+
+  Lemma Forall2_join {B} (P : A → B → Prop) ls1 ls2 :
+    Forall2 (Forall2 P) ls1 ls2 →
+    Forall2 P (mjoin ls1) (mjoin ls2).
+  Proof. induction 1; simpl; auto using Forall2_app. Qed.
 End list_ret_join.
 
 Ltac simplify_list_fmap_equality := repeat
@@ -1126,14 +1762,18 @@ Section same_length.
     | same_length_cons x y l k :
       same_length l k → same_length (x :: l) (y :: k).
 
-  Lemma same_length_length l k :
-    same_length l k ↔ length l = length k.
+  Lemma same_length_length_1 l k :
+    same_length l k → length l = length k.
+  Proof. induction 1; simpl; auto. Qed.
+  Lemma same_length_length_2 l k :
+    length l = length k → same_length l k.
   Proof.
-    split.
-    * induction 1; simpl; auto.
-    * revert k. induction l; intros [|??]; try discriminate;
+    revert k. induction l; intros [|??]; try discriminate;
       constructor; auto with arith.
   Qed.
+  Lemma same_length_length l k :
+    same_length l k ↔ length l = length k.
+  Proof. split; auto using same_length_length_1, same_length_length_2. Qed.
 
   Lemma same_length_lookup l k i :
     same_length l k → is_Some (l !! i) → is_Some (k !! i).
@@ -1143,14 +1783,34 @@ Section same_length.
     intros E. by rewrite E.
   Qed.
 
+  Lemma Forall2_same_length (P : A → B → Prop) l1 l2 :
+    Forall2 P l1 l2 →
+    same_length l1 l2.
+  Proof. intro. eapply same_length_length, Forall2_length; eauto. Qed.
   Lemma Forall2_app_inv (P : A → B → Prop) l1 l2 k1 k2 :
     same_length l1 k1 →
     Forall2 P (l1 ++ l2) (k1 ++ k2) → Forall2 P l2 k2.
   Proof. induction 1. done. inversion 1; subst; auto. Qed.
+
+  Lemma same_length_Forall2 l1 l2 :
+    same_length l1 l2 ↔ Forall2 (λ _ _, True) l1 l2.
+  Proof. split; induction 1; constructor; auto. Qed.
+
+  Lemma same_length_take l1 l2 n :
+    same_length l1 l2 →
+    same_length (take n l1) (take n l2).
+  Proof. rewrite !same_length_Forall2. apply Forall2_take. Qed.
+  Lemma same_length_drop l1 l2 n :
+    same_length l1 l2 →
+    same_length (drop n l1) (drop n l2).
+  Proof. rewrite !same_length_Forall2. apply Forall2_drop. Qed.
+  Lemma same_length_resize l1 l2 x1 x2 n :
+    same_length (resize n x1 l1) (resize n x2 l2).
+  Proof. apply same_length_length. by rewrite !resize_length. Qed.
 End same_length.
 
 Instance: ∀ A, Reflexive (@same_length A A).
-Proof. intros A l. induction l; try constructor; auto. Qed.
+Proof. intros A l. induction l; constructor; auto. Qed.
 
 (** * Zipping lists *)
 Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C :=
@@ -1198,7 +1858,7 @@ Section zip_with.
     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 :
+  Lemma Forall_zip_with_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).
@@ -1206,8 +1866,7 @@ Section zip_with.
     intros Hl1. revert l2.
     induction Hl1; destruct 1; simpl in *; auto.
   Qed.
-
-  Lemma zip_with_Forall_snd (P : B → Prop) (Q : C → Prop) l1 l2 :
+  Lemma Forall_zip_with_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).
@@ -1300,6 +1959,144 @@ Proof.
   by apply IH.
 Qed.
 
+(** * Permutations *)
+Fixpoint interleave {A} (x : A) (l : list A) : list (list A) :=
+  match l with
+  | [] => [ [x] ]
+  | y :: l => (x :: y :: l) :: ((y ::) <$> interleave x l)
+  end.
+Fixpoint permutations {A} (l : list A) : list (list A) :=
+  match l with
+  | [] => [ [] ]
+  | x :: l => permutations l ≫= interleave x
+  end.
+
+Section permutations.
+  Context {A : Type}.
+
+  Lemma interleave_cons (x : A) (l : list A) :
+    x :: l ∈ interleave x l.
+  Proof. destruct l; simpl; rewrite elem_of_cons; auto. Qed.
+  Lemma interleave_Permutation (x : A) (l l' : list A) :
+    l' ∈ interleave x l → Permutation l' (x :: l).
+  Proof.
+    revert l'. induction l as [|y l IH]; intros l'; simpl.
+    * rewrite elem_of_list_singleton. intros. by subst.
+    * rewrite elem_of_cons, elem_of_list_fmap.
+      intros [?|[? [? H]]]; subst.
+      + by constructor.
+      + rewrite (IH _ H). constructor.
+  Qed.
+
+  Lemma permutations_refl (l : list A) :
+    l ∈ permutations l.
+  Proof.
+    induction l; simpl.
+    * by apply elem_of_list_singleton.
+    * apply elem_of_list_bind. eauto using interleave_cons.
+  Qed.
+  Lemma permutations_skip (x : A) (l l' : list A) : 
+    l ∈ permutations l' →
+    x :: l ∈ permutations (x :: l').
+  Proof.
+    intros Hl. simpl. apply elem_of_list_bind.
+    eauto using interleave_cons.
+  Qed.
+  Lemma permutations_swap (x y : A) (l : list A) : 
+    y :: x :: l ∈ permutations (x :: y :: l).
+  Proof.
+    simpl. apply elem_of_list_bind.
+    exists (y :: l). split; simpl.
+    * destruct l; simpl; rewrite !elem_of_cons; auto.
+    * apply elem_of_list_bind. simpl.
+      eauto using interleave_cons, permutations_refl.
+  Qed.
+  Lemma permutations_nil (l : list A) :
+    l ∈ permutations [] ↔ l = [].
+  Proof. simpl. by rewrite elem_of_list_singleton. Qed.
+
+  Lemma interleave_interleave_toggle (x1 x2 : A) (l1 l2 l3 : list A) :
+    l1 ∈ interleave x1 l2 →
+    l2 ∈ interleave x2 l3 → ∃ l4,
+      l1 ∈ interleave x2 l4 ∧ l4 ∈ interleave x1 l3.
+  Proof.
+    revert l1 l2. induction l3 as [|y l3 IH]; intros l1 l2; simpl.
+    { intros Hl1 Hl2.
+      rewrite elem_of_list_singleton in Hl2. subst. simpl in Hl1.
+      rewrite elem_of_cons, elem_of_list_singleton in Hl1.
+      exists [x1]. simpl.
+      rewrite elem_of_cons, !elem_of_list_singleton. tauto. }
+    rewrite elem_of_cons, elem_of_list_fmap.
+    intros Hl1 [? | [l2' [??]]]; subst; simpl in *.
+    * rewrite !elem_of_cons, elem_of_list_fmap in Hl1.
+      destruct Hl1 as [? | [? | [l4 [??]]]]; subst.
+      + exists (x1 :: y :: l3). simpl. rewrite !elem_of_cons. tauto.
+      + exists (x1 :: y :: l3). simpl. rewrite !elem_of_cons. tauto.
+      + exists l4. simpl. rewrite elem_of_cons. auto using interleave_cons.
+    * rewrite elem_of_cons, elem_of_list_fmap in Hl1.
+      destruct Hl1 as [? | [l1' [??]]]; subst.
+      + exists (x1 :: y :: l3). simpl.
+        rewrite !elem_of_cons, !elem_of_list_fmap.
+        split; [| by auto]. right. right. exists (y :: l2').
+        rewrite elem_of_list_fmap. naive_solver.
+      + destruct (IH l1' l2') as [l4 [??]]; auto.
+        exists (y :: l4). simpl.
+        rewrite !elem_of_cons, !elem_of_list_fmap. naive_solver.
+  Qed.
+  Lemma permutations_interleave_toggle (x : A) (l1 l2 l3 : list A) :
+    l1 ∈ permutations l2 →
+    l2 ∈ interleave x l3 → ∃ l4,
+      l1 ∈ interleave x l4 ∧ l4 ∈ permutations l3.
+  Proof.
+    revert l1 l2. induction l3 as [|y l3 IH]; intros l1 l2; simpl.
+    { intros Hl1 Hl2. eexists []. simpl.
+      split; [| by rewrite elem_of_list_singleton].
+      rewrite elem_of_list_singleton in Hl2.
+      by rewrite Hl2 in Hl1. }
+    rewrite elem_of_cons, elem_of_list_fmap.
+    intros Hl1 [? | [l2' [? Hl2']]]; subst; simpl in *.
+    * rewrite elem_of_list_bind in Hl1.
+      destruct Hl1 as [l1' [??]]. by exists l1'.
+    * rewrite elem_of_list_bind in Hl1.
+      setoid_rewrite elem_of_list_bind.
+      destruct Hl1 as [l1' [??]].
+      destruct (IH l1' l2') as [l1'' [??]]; auto.
+      destruct (interleave_interleave_toggle y x l1 l1' l1'') as [? [??]]; eauto.
+  Qed.
+  Lemma permutations_trans (l1 l2 l3 : list A) :
+    l1 ∈ permutations l2 →
+    l2 ∈ permutations l3 →
+    l1 ∈ permutations l3.
+  Proof.
+    revert l1 l2. induction l3 as [|x l3 IH]; intros l1 l2; simpl.
+    * intros Hl1 Hl2. rewrite elem_of_list_singleton in Hl2.
+      by rewrite Hl2 in Hl1.
+    * rewrite !elem_of_list_bind. intros Hl1 [l2' [Hl2 Hl2']].
+      destruct (permutations_interleave_toggle x l1 l2 l2') as [? [??]]; eauto.
+  Qed.
+
+  Lemma permutations_Permutation (l l' : list A) :
+    l' ∈ permutations l ↔ Permutation l l'.
+  Proof.
+    split.
+    * revert l'. induction l; simpl; intros l''.
+      + rewrite elem_of_list_singleton.
+        intros. subst. constructor.
+      + rewrite elem_of_list_bind. intros [l' [Hl'' ?]].
+        rewrite (interleave_Permutation _ _ _ Hl'').
+        constructor; auto.
+    * induction 1; eauto using permutations_refl,
+        permutations_skip, permutations_swap, permutations_trans.
+  Qed.
+
+  Global Instance Permutation_dec `{∀ x y : A, Decision (x = y)}
+    (l1 l2 : list A) : Decision (Permutation l1 l2).
+  Proof.
+    refine (cast_if (decide (l2 ∈ permutations l1)));
+      by rewrite <-permutations_Permutation.
+  Defined.
+End permutations.
+
 (** * Set operations on lists *)
 Section list_set_operations.
   Context {A} {dec : ∀ x y : A, Decision (x = y)}.
@@ -1349,4 +2146,37 @@ Section list_set_operations.
     * constructor. rewrite elem_of_list_intersection; intuition. done.
     * done.
   Qed.
+
+  Definition list_intersection_with (f : A → A → option A) :
+      list A → list A → list A :=
+    fix go l k :=
+    match l with
+    | [] => []
+    | x :: l => foldr (λ y,
+       match f x y with None => id | Some z => (z ::) end) (go l k) k
+    end.
+  Lemma elem_of_list_intersection_with f l k x :
+    x ∈ list_intersection_with f l k ↔ ∃ x1 x2,
+      x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x.
+  Proof.
+    split.
+    * induction l as [|x1 l IH]; simpl.
+      + by rewrite elem_of_nil.
+      + intros Hx. setoid_rewrite elem_of_cons.
+        cut ((∃ x2, x2 ∈ k ∧ f x1 x2 = Some x)
+          ∨ x ∈ list_intersection_with f l k).
+        { naive_solver. }
+        clear IH. revert Hx. generalize (list_intersection_with f l k).
+        induction k; simpl; [by auto|].
+        case_match; setoid_rewrite elem_of_cons; naive_solver.
+    * intros (x1 & x2 & Hx1 & Hx2 & Hx).
+      induction Hx1 as [x1 | x1 ? l ? IH]; simpl.
+      + generalize (list_intersection_with f l k).
+        induction Hx2; simpl; [by rewrite Hx; left |].
+        case_match; simpl; try setoid_rewrite elem_of_cons; auto.
+      + generalize (IH Hx). clear Hx IH Hx2.
+        generalize (list_intersection_with f l k).
+        induction k; simpl; intros; [done |].
+        case_match; simpl; rewrite ?elem_of_cons; auto.
+  Qed.
 End list_set_operations.
diff --git a/theories/listset.v b/theories/listset.v
index eeb4d263727e2c15bee28c570ddf372c3ff5cbe4..21da87526f4ea6fd31167f0c7b3333f06e41c739 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -20,29 +20,44 @@ Instance listset_empty: Empty (listset A) :=
 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).
+  match l, k with
+  | Listset l', Listset k' => Listset (l' ++ k')
+  end.
 
 Global Instance: SimpleCollection A (listset A).
 Proof.
   split.
   * by apply not_elem_of_nil.
   * by apply elem_of_list_singleton.
-  * intros. apply elem_of_app.
+  * intros [?] [?]. apply elem_of_app.
 Qed.
 
 Context `{∀ x y : A, Decision (x = y)}.
 
 Instance listset_intersection: Intersection (listset A) := λ l k,
-  Listset (list_intersection (listset_car l) (listset_car k)).
+  match l, k with
+  | Listset l', Listset k' => Listset (list_intersection l' k')
+  end.
 Instance listset_difference: Difference (listset A) := λ l k,
-  Listset (list_difference (listset_car l) (listset_car k)).
+  match l, k with
+  | Listset l', Listset k' => Listset (list_difference l' k')
+  end.
+Instance listset_intersection_with: IntersectionWith A (listset A) := λ f l k,
+  match l, k with
+  | Listset l', Listset k' => Listset (list_intersection_with f l' k')
+  end.
+Instance listset_filter: Filter A (listset A) := λ P _ l,
+  match l with
+  | Listset l' => Listset (filter P l')
+  end.
 
 Global Instance: Collection A (listset A).
 Proof.
   split.
   * apply _.
-  * intros. apply elem_of_list_intersection.
-  * intros. apply elem_of_list_difference.
+  * intros [?] [?]. apply elem_of_list_intersection.
+  * intros [?] [?]. apply elem_of_list_difference.
+  * intros ? [?] [?]. apply elem_of_list_intersection_with.
 Qed.
 
 Instance listset_elems: Elements A (listset A) :=
@@ -52,6 +67,7 @@ Global Instance: FinCollection A (listset A).
 Proof.
   split.
   * apply _.
+  * intros [?] ??. apply elem_of_list_filter.
   * symmetry. apply elem_of_remove_dups.
   * intros. apply remove_dups_nodup.
 Qed.
@@ -69,27 +85,35 @@ Hint Extern 1 (Union (listset _)) =>
   eapply @listset_union : typeclass_instances.
 Hint Extern 1 (Intersection (listset _)) =>
   eapply @listset_intersection : typeclass_instances.
+Hint Extern 1 (IntersectionWith _ (listset _)) =>
+  eapply @listset_intersection_with : typeclass_instances.
 Hint Extern 1 (Difference (listset _)) =>
   eapply @listset_difference : typeclass_instances.
 Hint Extern 1 (Elements _ (listset _)) =>
   eapply @listset_elems : typeclass_instances.
+Hint Extern 1 (Filter _ (listset _)) =>
+  eapply @listset_filter : typeclass_instances.
 
 Instance listset_ret: MRet listset := λ A x,
   {[ x ]}.
 Instance listset_fmap: FMap listset := λ A B f l,
-  Listset (f <$> listset_car l).
+  match l with
+  | Listset l' => Listset (f <$> l')
+  end.
 Instance listset_bind: MBind listset := λ A B f l,
-  Listset (mbind (listset_car ∘ f) (listset_car l)).
+  match l with
+  | Listset l' => Listset (mbind (listset_car ∘ f) l')
+  end.
 Instance listset_join: MJoin listset := λ A, mbind id.
 
 Instance: CollectionMonad listset.
 Proof.
   split.
   * intros. apply _.
-  * intros. apply elem_of_list_bind.
+  * intros ??? [?] ?. apply elem_of_list_bind.
   * intros. apply elem_of_list_ret.
-  * intros. apply elem_of_list_fmap.
-  * intros ?? [l].
+  * intros ??? [?]. apply elem_of_list_fmap.
+  * intros ? [?] ?.
     unfold mjoin, listset_join, elem_of, listset_elem_of.
     simpl. by rewrite elem_of_list_bind.
 Qed.
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
new file mode 100644
index 0000000000000000000000000000000000000000..a63c969a5f1149fd13471c81502c4760b651b8ab
--- /dev/null
+++ b/theories/listset_nodup.v
@@ -0,0 +1,103 @@
+(* 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. *)
+Require Export base decidable collections list.
+
+Record listset_nodup A := ListsetNoDup {
+  listset_nodup_car : list A;
+  listset_nodup_prf : NoDup listset_nodup_car
+}.
+Arguments ListsetNoDup {_} _ _.
+Arguments listset_nodup_car {_} _.
+Arguments listset_nodup_prf {_} _.
+
+Section list_collection.
+Context {A : Type} `{∀ x y : A, Decision (x = y)}.
+
+Notation C := (listset_nodup A).
+Notation LS := ListsetNoDup.
+
+Instance listset_nodup_elem_of: ElemOf A C := λ x l,
+  x ∈ listset_nodup_car l.
+Instance listset_nodup_empty: Empty C :=
+  LS [] (@NoDup_nil_2 _).
+Instance listset_nodup_singleton: Singleton A C := λ x,
+  LS [x] (NoDup_singleton x).
+Instance listset_nodup_difference: Difference C := λ l k,
+  LS _ (list_difference_nodup _ (listset_nodup_car k) (listset_nodup_prf l)).
+
+Definition listset_nodup_union_raw (l k : list A) : list A :=
+  list_difference l k ++ k.
+Lemma elem_of_listset_nodup_union_raw l k x :
+  x ∈ listset_nodup_union_raw l k ↔ x ∈ l ∨ x ∈ k.
+Proof.
+  unfold listset_nodup_union_raw.
+  rewrite elem_of_app, elem_of_list_difference.
+  intuition. case (decide (x ∈ k)); intuition.
+Qed.
+Lemma listset_nodup_union_raw_nodup l k :
+  NoDup l → NoDup k → NoDup (listset_nodup_union_raw l k).
+Proof.
+  intros. apply NoDup_app. repeat split.
+  * by apply list_difference_nodup.
+  * intro. rewrite elem_of_list_difference. intuition.
+  * done.
+Qed.
+Instance listset_nodup_union: Union C := λ l k,
+  LS _ (listset_nodup_union_raw_nodup _ _
+     (listset_nodup_prf l) (listset_nodup_prf k)).
+Instance listset_nodup_intersection: Intersection C := λ l k,
+  LS _ (list_intersection_nodup _
+     (listset_nodup_car k) (listset_nodup_prf l)).
+Instance listset_nodup_intersection_with:
+    IntersectionWith A C := λ f l k,
+  LS (remove_dups
+      (list_intersection_with f (listset_nodup_car l) (listset_nodup_car k)))
+    (remove_dups_nodup _).
+Instance listset_nodup_filter: Filter A C :=
+  λ P _ l, LS _ (filter_nodup P _ (listset_nodup_prf l)).
+
+Global Instance: Collection A C.
+Proof.
+  split; [split | | |].
+  * by apply not_elem_of_nil.
+  * by apply elem_of_list_singleton.
+  * intros. apply elem_of_listset_nodup_union_raw.
+  * intros. apply elem_of_list_intersection.
+  * intros. apply elem_of_list_difference.
+  * intros. unfold intersection_with, listset_nodup_intersection_with,
+      elem_of, listset_nodup_elem_of. simpl.
+    rewrite elem_of_remove_dups.
+    by apply elem_of_list_intersection_with.
+Qed.
+
+Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
+
+Global Instance: FinCollection A C.
+Proof.
+  split.
+  * apply _.
+  * intros. apply elem_of_list_filter.
+  * done.
+  * by intros [??].
+Qed.
+End list_collection.
+
+Hint Extern 1 (ElemOf _ (listset_nodup _)) =>
+  eapply @listset_nodup_elem_of : typeclass_instances.
+Hint Extern 1 (Empty (listset_nodup _)) =>
+  eapply @listset_nodup_empty : typeclass_instances.
+Hint Extern 1 (Singleton _ (listset_nodup _)) =>
+  eapply @listset_nodup_singleton : typeclass_instances.
+Hint Extern 1 (Union (listset_nodup _)) =>
+  eapply @listset_nodup_union : typeclass_instances.
+Hint Extern 1 (Intersection (listset_nodup _)) =>
+  eapply @listset_nodup_intersection : typeclass_instances.
+Hint Extern 1 (Difference (listset_nodup _)) =>
+  eapply @listset_nodup_difference : typeclass_instances.
+Hint Extern 1 (Elements _ (listset_nodup _)) =>
+  eapply @listset_nodup_elems : typeclass_instances.
+Hint Extern 1 (Filter _ (listset_nodup _)) =>
+  eapply @listset_nodup_filter : typeclass_instances.
diff --git a/theories/nmap.v b/theories/nmap.v
index 210cfe03923c49e936b3de62fdbd737e8ebe645a..312e9ee9b9e52fae96f934b56095504021691c21 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -17,21 +17,22 @@ Instance Pmap_dec `{∀ x y : A, Decision (x = y)} :
 Proof. solve_decision. Defined.
 
 Instance Nempty {A} : Empty (Nmap A) := NMap None ∅.
-Instance Nlookup {A} : Lookup N (Nmap A) A := λ i t,
+Instance Nlookup {A} : Lookup N A (Nmap A) := λ i t,
   match i with
   | N0 => Nmap_0 t
   | Npos p => Nmap_pos t !! p
   end.
-Instance Npartial_alter {A} : PartialAlter N (Nmap A) A := λ f i t,
+Instance Npartial_alter {A} : PartialAlter N A (Nmap A) := λ f i t,
   match i, t with
   | N0, NMap o t => NMap (f o) t
   | Npos p, NMap o t => NMap o (partial_alter f p t)
   end.
-Instance Ndom {A} : Dom N (Nmap A) := λ C _ _ _ t,
+Instance Nto_list {A} : FinMapToList N A (Nmap A) := λ t,
   match t with
-  | NMap o t => option_case (λ _, {[ 0 ]}) ∅ o ∪ (Pdom_raw Npos (`t))
+  | NMap o t => option_case (λ x, [(0,x)]) [] o ++
+     (fst_map Npos <$> finmap_to_list t)
   end.
-Instance Nmerge: Merge Nmap := λ A f t1 t2,
+Instance Nmerge {A} : Merge A (Nmap A) := λ f t1 t2,
   match t1, t2 with
   | NMap o1 t1, NMap o2 t2 => NMap (f o1 o2) (merge f t1 t2)
   end.
@@ -53,9 +54,26 @@ 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.
-    rewrite elem_of_union, Plookup_raw_dom.
-    destruct o, n; esolve_elem_of (inv_is_Some; eauto).
+  * intros ? [[x|] t]; unfold finmap_to_list; simpl.
+    + constructor.
+      - rewrite elem_of_list_fmap. by intros [[??] [??]].
+      - rewrite (NoDup_fmap _). apply finmap_to_list_nodup.
+    + rewrite (NoDup_fmap _). apply finmap_to_list_nodup.
+  * intros ? t i x. unfold finmap_to_list. split.
+    + destruct t as [[y|] t]; simpl.
+      - rewrite elem_of_cons, elem_of_list_fmap.
+        intros [? | [[??] [??]]]; simplify_equality; simpl; [done |].
+        by apply elem_of_finmap_to_list.
+      - rewrite elem_of_list_fmap.
+        intros [[??] [??]]; simplify_equality; simpl.
+        by apply elem_of_finmap_to_list.
+    + destruct t as [[y|] t]; simpl.
+      - rewrite elem_of_cons, elem_of_list_fmap.
+        destruct i as [|i]; simpl; [intuition congruence |].
+        intros. right. exists (i, x). by rewrite elem_of_finmap_to_list.
+      - rewrite elem_of_list_fmap.
+        destruct i as [|i]; simpl; [done |].
+        intros. exists (i, x). by rewrite elem_of_finmap_to_list.
   * 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 8c39e4e8a758626de9ba40f0155c77e5db2781e6..dda95af2b6ed234b28a6278305f5dcb0a4a31b6b 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -31,10 +31,23 @@ Proof. auto with arith. Qed.
 Lemma lt_n_SSS n : n < S (S (S n)).
 Proof. auto with arith. Qed.
 
+Definition sum_list_with {A} (f : A → nat) : list A → nat :=
+  fix go l :=
+  match l with
+  | [] => 0
+  | x :: l => f x + go l
+  end.
+Notation sum_list := (sum_list_with id).
+
 Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec.
 Notation "(~0)" := xO (only parsing) : positive_scope.
 Notation "(~1)" := xI (only parsing) : positive_scope.
 
+Instance: Injective (=) (=) xO.
+Proof. by injection 1. Qed.
+Instance: Injective (=) (=) xI.
+Proof. by injection 1. Qed.
+
 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.
@@ -46,6 +59,9 @@ 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: Injective (=) (=) Npos.
+Proof. by injection 1. Qed.
+
 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
diff --git a/theories/option.v b/theories/option.v
index 3032b6f4b8b4e127c21bd4add3bb106a02e17b21..455d1a73ea7f084e84f3700a8936ab6d8a0c1434 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -22,9 +22,9 @@ Definition option_case {A B} (f : A → B) (b : B) (x : option A) : B :=
   | Some a => f a
   end.
 
-(** The [maybe] function allows us to get the value out of the option type
-by specifying a default value. *)
-Definition maybe {A} (a : A) (x : option A) : A :=
+(** The [from_option] function allows us to get the value out of the option
+type by specifying a default value. *)
+Definition from_option {A} (a : A) (x : option A) : A :=
   match x with
   | None => a
   | Some b => b
@@ -62,22 +62,31 @@ Ltac inv_is_Some := repeat
   | H : is_Some _ |- _ => inversion H; clear H; subst
   end.
 
-Definition is_Some_sigT `(x : option A) : is_Some x → { a | x = Some a } :=
+Definition is_Some_proj `{x : option A} : is_Some x → A :=
   match x with
+  | Some a => λ _, a
   | None => False_rect _ ∘ is_Some_None
-  | Some a => λ _, a ↾ eq_refl
   end.
-
+Definition Some_dec `(x : option A) : { a | x = Some a } + { x = None } :=
+  match x return { a | x = Some a } + { x = None } with
+  | Some a => inleft (a ↾ eq_refl _)
+  | None => inright 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.
+Instance None_dec `(x : option A) : Decision (x = None) :=
+  match x with
+  | Some x => right (Some_ne_None x)
+  | None => left eq_refl
+  end.
 
 Lemma eq_None_not_Some `(x : option A) : x = None ↔ ¬is_Some x.
 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.
+Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed.
 
 Lemma make_eq_Some {A} (x : option A) a :
   is_Some x → (∀ b, x = Some b → b = a) → x = Some a.
@@ -90,17 +99,17 @@ Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)}
   | Some a =>
     match y with
     | Some b =>
-      match dec a b with
-      | left H => left (f_equal _ H)
-      | right H => right (H ∘ injective Some _ _)
-      end
+       match dec a b with
+       | left H => left (f_equal _ H)
+       | right H => right (H ∘ injective Some _ _)
+       end
     | None => right (Some_ne_None _)
     end
   | None =>
-    match y with
-    | Some _ => right (None_ne_Some _)
-    | None => left eq_refl
-    end
+     match y with
+     | Some _ => right (None_ne_Some _)
+     | None => left eq_refl
+     end
   end.
 
 (** * Monadic operations *)
@@ -126,97 +135,132 @@ Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) :
   x = None ↔ f <$> x = None.
 Proof. unfold fmap, option_fmap. by destruct x. Qed.
 
+Lemma option_bind_assoc {A B C} (f : A → option B)
+    (g : B → option C) (x : option A) : (x ≫= f) ≫= g = x ≫= (mbind g ∘ f).
+Proof. by destruct x; simpl. Qed.
+
 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 |- _ =>
-    let x := fresh in evar (x:A);
-    let x' := eval unfold x in x in clear x;
+  | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
     let Hx := fresh in
-    assert (o = Some x') as Hx by tac;
+    first
+      [ let x := fresh in evar (x:A);
+        let x' := eval unfold x in x in clear x;
+        assert (o = Some x') as Hx by tac
+      | assert (o = None) as Hx by tac ];
     rewrite Hx in H; clear Hx
+  | H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ =>
+    let Hx := fresh in
+    first
+      [ let x := fresh in evar (x:A);
+        let x' := eval unfold x in x in clear x;
+        assert (o = Some x') as Hx by tac
+      | assert (o = None) as Hx by tac ];
+    rewrite Hx in H; clear Hx
+  | H : context [ match ?o with _ => _ end ] |- _ =>
+    match type of o with
+    | option ?A =>
+      let Hx := fresh in
+      first
+        [ let x := fresh in evar (x:A);
+          let x' := eval unfold x in x in clear x;
+          assert (o = Some x') as Hx by tac
+        | assert (o = None) as Hx by tac ];
+      rewrite Hx in H; clear Hx
+    end
   | H : mbind (M:=option) ?f ?o = ?x |- _ =>
     match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
     match x with Some _ => idtac | None => idtac | _ => fail 1 end;
     destruct o eqn:?
-  | |- mbind (M:=option) (A:=?A) ?f ?o = ?x =>
-    let x := fresh in evar (x:A);
-    let x' := eval unfold x in x in clear x;
+  | H : ?x = mbind (M:=option) ?f ?o |- _ =>
+    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
+    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
+    destruct o eqn:?
+  | H : fmap (M:=option) ?f ?o = ?x |- _ =>
+    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
+    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
+    destruct o eqn:?
+  | H : ?x = fmap (M:=option) ?f ?o |- _ =>
+    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
+    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
+    destruct o eqn:?
+  | |- context [mbind (M:=option) (A:=?A) ?f ?o] =>
     let Hx := fresh in
-    assert (o = Some x') as Hx by tac;
+    first
+      [ let x := fresh in evar (x:A);
+        let x' := eval unfold x in x in clear x;
+        assert (o = Some x') as Hx by tac
+      | assert (o = None) as Hx by tac ];
     rewrite Hx; clear Hx
+  | |- context [fmap (M:=option) (A:=?A) ?f ?o] =>
+    let Hx := fresh in
+    first
+      [ let x := fresh in evar (x:A);
+        let x' := eval unfold x in x in clear x;
+        assert (o = Some x') as Hx by tac
+      | assert (o = None) as Hx by tac ];
+    rewrite Hx; clear Hx
+  | |- context [ match ?o with _ => _ end ] =>
+    match type of o with
+    | option ?A =>
+      let Hx := fresh in
+      first
+        [ let x := fresh in evar (x:A);
+          let x' := eval unfold x in x in clear x;
+          assert (o = Some x') as Hx by tac
+        | assert (o = None) as Hx by tac ];
+      rewrite Hx; clear Hx
+    end
   | 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
+  | H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ =>
+    assert (y = x) by congruence; clear H2
+  | H1 : ?o = Some ?x, H2 : ?o = None |- _ =>
+    congruence
   end.
-Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto.
+Tactic Notation "simplify_option_equality" :=
+  simplify_option_equality by eauto.
+
+Hint Extern 100 => simplify_option_equality : simplify_option_equality.
 
 (** * Union, intersection and difference *)
-Instance option_union: UnionWith option := λ A f x y,
+Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
   match x, y with
-  | Some a, Some b => Some (f a b)
+  | Some a, Some b => f a b
   | Some a, None => Some a
   | None, Some b => Some b
   | None, None => None
   end.
-Instance option_intersection: IntersectionWith option := λ A f x y,
+Instance option_intersection_with {A} :
+    IntersectionWith A (option A) := λ f x y,
   match x, y with
-  | Some a, Some b => Some (f a b)
+  | Some a, Some b => f a b
   | _, _ => None
   end.
-Instance option_difference: DifferenceWith option := λ A f x y,
+Instance option_difference_with {A} :
+    DifferenceWith A (option A) := λ f x y,
   match x, y with
   | Some a, Some b => f a b
   | Some a, None => Some a
   | None, _ => None
   end.
 
-Section option_union_intersection.
-  Context {A} (f : A → A → A).
+Section option_union_intersection_difference.
+  Context {A} (f : A → A → option A).
 
   Global Instance: LeftId (=) None (union_with f).
   Proof. by intros [?|]. Qed.
   Global Instance: RightId (=) None (union_with f).
   Proof. by intros [?|]. Qed.
   Global Instance: Commutative (=) f → Commutative (=) (union_with f).
-  Proof.
-    intros ? [?|] [?|]; compute; try reflexivity.
-    by rewrite (commutative f).
-  Qed.
-  Global Instance: Associative (=) f → Associative (=) (union_with f).
-  Proof.
-    intros ? [?|] [?|] [?|]; compute; try reflexivity.
-    by rewrite (associative f).
-  Qed.
-  Global Instance: Idempotent (=) f → Idempotent (=) (union_with f).
-  Proof.
-    intros ? [?|]; compute; try reflexivity.
-    by rewrite (idempotent f).
-  Qed.
-
+  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
   Global Instance: Commutative (=) f → Commutative (=) (intersection_with f).
-  Proof.
-    intros ? [?|] [?|]; compute; try reflexivity.
-    by rewrite (commutative f).
-  Qed.
-  Global Instance: Associative (=) f → Associative (=) (intersection_with f).
-  Proof.
-    intros ? [?|] [?|] [?|]; compute; try reflexivity.
-    by rewrite (associative f).
-  Qed.
-  Global Instance: Idempotent (=) f → Idempotent (=) (intersection_with f).
-  Proof.
-    intros ? [?|]; compute; try reflexivity.
-    by rewrite (idempotent f).
-  Qed.
-End option_union_intersection.
-
-Section option_difference.
-  Context {A} (f : A → A → option A).
-
+  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
   Global Instance: RightId (=) None (difference_with f).
   Proof. by intros [?|]. Qed.
-End option_difference.
+End option_union_intersection_difference.
diff --git a/theories/orders.v b/theories/orders.v
index f80147096f15d50c60aa9798cd09fa7c789374c4..89c4554122d4f25206b541d0573c1f960c5d5b92 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -28,10 +28,48 @@ Section preorder.
     * transitivity y1. tauto. transitivity y2; tauto.
   Qed.
 
+  Global Instance preorder_subset: Subset A := λ X Y, X ⊆ Y ∧ Y ⊈ X.
+  Lemma subset_spec X Y : X ⊂ Y ↔ X ⊆ Y ∧ Y ⊈ X.
+  Proof. done. Qed.
+
+  Lemma subset_subseteq X Y : X ⊂ Y → X ⊆ Y.
+  Proof. by intros [? _]. Qed.
+  Lemma subset_trans_l X Y Z : X ⊂ Y → Y ⊆ Z → X ⊂ Z.
+  Proof.
+    intros [? Hxy] ?. split.
+    * by transitivity Y.
+    * contradict Hxy. by transitivity Z.
+  Qed.
+  Lemma subset_trans_r X Y Z : X ⊆ Y → Y ⊂ Z → X ⊂ Z.
+  Proof.
+    intros ? [? Hyz]. split.
+    * by transitivity Y.
+    * contradict Hyz. by transitivity X.
+  Qed.
+
+  Global Instance: StrictOrder (⊂).
+  Proof.
+    split.
+    * firstorder.
+    * eauto using subset_trans_r, subset_subseteq.
+  Qed.
+  Global Instance: Proper ((≡) ==> (≡) ==> iff) (⊂).
+  Proof. unfold subset, preorder_subset. solve_proper. Qed.
+
   Context `{∀ X Y : A, Decision (X ⊆ Y)}.
   Global Instance preorder_equiv_dec_slow (X Y : A) :
     Decision (X ≡ Y) | 100 := _.
+  Global Instance preorder_subset_dec_slow (X Y : A) :
+    Decision (X ⊂ Y) | 100 := _.
+
+  Lemma subseteq_inv X Y : X ⊆ Y → X ⊂ Y ∨ X ≡ Y.
+  Proof.
+    destruct (decide (Y ⊆ X)).
+    * by right.
+    * by left.
+  Qed.
 End preorder.
+
 Typeclasses Opaque preorder_equiv.
 Hint Extern 0 (@Equivalence _ (≡)) =>
   class_apply preorder_equivalence : typeclass_instances.
diff --git a/theories/pmap.v b/theories/pmap.v
index d8388187bf4e5e6ef5d00c179389a59aadf50e88..b7c04de4839d8bc00ff95769746e3d68059a237f 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -79,18 +79,18 @@ 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.
 
-Instance Plookup_raw {A} : Lookup positive (Pmap_raw A) A :=
+Instance Plookup_raw {A} : Lookup positive A (Pmap_raw 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
-    end
+     match i with
+     | 1 => o
+     | i~0 => @lookup _ _ _ Plookup_raw i l
+     | i~1 => @lookup _ _ _ Plookup_raw i r
+     end
   end.
-Instance Plookup {A} : Lookup positive (Pmap A) A := λ i t, `t !! i.
+Instance Plookup {A} : Lookup positive A (Pmap A) := λ i t, `t !! i.
 
 Lemma Plookup_raw_empty {A} i : (∅ : Pmap_raw A) !! i = None.
 Proof. by destruct i. Qed.
@@ -179,20 +179,20 @@ Ltac Pnode_canon_rewrite := repeat (
   rewrite Pnode_canon_lookup_xO ||
   rewrite Pnode_canon_lookup_xI).
 
-Instance Ppartial_alter_raw {A} : PartialAlter positive (Pmap_raw A) A :=
+Instance Ppartial_alter_raw {A} : PartialAlter positive A (Pmap_raw A) :=
   fix go f i t {struct t} : Pmap_raw A :=
   match t with
   | Pleaf =>
-    match f None with
-    | None => Pleaf
-    | Some x => Psingleton_raw i x
-    end
+     match f None with
+     | None => Pleaf
+     | Some x => Psingleton_raw i x
+     end
   | Pnode l o r =>
-    match i with
-    | 1 => Pnode_canon l (f o) 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
+     match i with
+     | 1 => Pnode_canon l (f o) 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.
 
 Lemma Ppartial_alter_raw_wf {A} f i (t : Pmap_raw A) :
@@ -204,7 +204,7 @@ Proof.
   * intros [?|?|]; simpl; intuition.
 Qed.
 
-Instance Ppartial_alter {A} : PartialAlter positive (Pmap A) A := λ f i t,
+Instance Ppartial_alter {A} : PartialAlter positive A (Pmap 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) :
@@ -257,35 +257,63 @@ Lemma Plookup_raw_fmap `(f : A → B) (t : Pmap_raw A) i :
   fmap f t !! i = fmap f (t !! i).
 Proof. revert i. induction t. done. by intros [?|?|]; simpl. Qed.
 
-(** The [dom] function is rather inefficient, but since we do not intend to
-use it for computation it does not really matter to us. *)
-Section dom.
-  Context `{Collection B D}.
-
-  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
-    end.
-
-  Lemma Plookup_raw_dom f `(t : Pmap_raw A) x :
-    x ∈ Pdom_raw f t ↔ ∃ i, x = f i ∧ is_Some (t !! i).
-  Proof.
-    split.
-    * 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 (first
-        [ by apply (IHl (f ∘ (~0)))
-        | by apply (IHr (f ∘ (~1)))
-        | inv_is_Some; eauto ]).
-  Qed.
-End dom.
-
-Global Instance Pdom {A} : Dom positive (Pmap A) := λ C _ _ _ t,
-  Pdom_raw id (`t).
+(** The [finmap_to_list] function is rather inefficient, but since we do not
+use it for computation at this moment, we do not care. *)
+Fixpoint Pto_list_raw {A} (t : Pmap_raw A) : list (positive * A) :=
+  match t with
+  | Pleaf => []
+  | Pnode l o r =>
+     option_case (λ x, [(1,x)]) [] o ++ 
+       (fst_map (~0) <$> Pto_list_raw l) ++ 
+       (fst_map (~1) <$> Pto_list_raw r)
+  end.
+
+Lemma Pto_list_raw_nodup {A} (t : Pmap_raw A) : NoDup (Pto_list_raw t).
+Proof.
+  induction t as [|? IHl [?|] ? IHr]; simpl.
+  * constructor.
+  * rewrite NoDup_cons, NoDup_app, !(NoDup_fmap _).
+    repeat split; trivial.
+    + rewrite elem_of_app, !elem_of_list_fmap.
+      intros [[[??] [??]] | [[??] [??]]]; simpl in *; simplify_equality.
+    + intro. rewrite !elem_of_list_fmap.
+      intros [[??] [??]] [[??] [??]]; simpl in *; simplify_equality.
+  * rewrite NoDup_app, !(NoDup_fmap _).
+    repeat split; trivial.
+    intro. rewrite !elem_of_list_fmap.
+    intros [[??] [??]] [[??] [??]]; simpl in *; simplify_equality.
+Qed.
+
+Lemma Pelem_of_to_list_raw {A} (t : Pmap_raw A) i x :
+  (i,x) ∈ Pto_list_raw t ↔ t !! i = Some x.
+Proof.
+  split.
+  * revert i. induction t as [|? IHl [?|] ? IHr]; intros i; simpl.
+    + by rewrite ?elem_of_nil.
+    + rewrite elem_of_cons, !elem_of_app, !elem_of_list_fmap.
+      intros [? | [[[??] [??]] | [[??] [??]]]]; naive_solver.
+    + rewrite !elem_of_app, !elem_of_list_fmap.
+      intros [[[??] [??]] | [[??] [??]]]; naive_solver.
+  * revert i. induction t as [|? IHl [?|] ? IHr]; simpl.
+    + done.
+    + intros i. rewrite elem_of_cons, elem_of_app.
+      destruct i as [i|i|]; simpl.
+      - right. right. rewrite elem_of_list_fmap.
+        exists (i,x); simpl; auto.
+      - right. left. rewrite elem_of_list_fmap.
+        exists (i,x); simpl; auto.
+      - left. congruence.
+    + intros i. rewrite elem_of_app.
+      destruct i as [i|i|]; simpl.
+      - right. rewrite elem_of_list_fmap.
+        exists (i,x); simpl; auto.
+      - left. rewrite elem_of_list_fmap.
+        exists (i,x); simpl; auto.
+      - done.
+Qed.
+
+Global Instance Pto_list {A} : FinMapToList positive A (Pmap A) :=
+  λ t, Pto_list_raw (`t).
 
 Fixpoint Pmerge_aux `(f : option A → option B) (t : Pmap_raw A) : Pmap_raw B :=
   match t with
@@ -306,21 +334,21 @@ Proof.
   intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
 Qed.
 
-Global Instance Pmerge_raw: Merge Pmap_raw :=
-  fix Pmerge_raw A f (t1 t2 : Pmap_raw A) : Pmap_raw A :=
+Global Instance Pmerge_raw {A} : Merge A (Pmap_raw A) :=
+  fix Pmerge_raw f (t1 t2 : Pmap_raw A) : Pmap_raw A :=
   match t1, t2 with
   | Pleaf, t2 => Pmerge_aux (f None) t2
   | t1, Pleaf => Pmerge_aux (flip f None) t1
   | Pnode l1 o1 r1, Pnode l2 o2 r2 =>
-     Pnode_canon (@merge _ Pmerge_raw _ f l1 l2)
-      (f o1 o2) (@merge _ Pmerge_raw _ f r1 r2)
+     Pnode_canon (@merge _ _ Pmerge_raw f l1 l2)
+      (f o1 o2) (@merge _ _ Pmerge_raw f r1 r2)
   end.
 Local Arguments Pmerge_aux _ _ _ _ : simpl never.
 
 Lemma Pmerge_wf {A} f (t1 t2 : Pmap_raw A) :
   Pmap_wf t1 → Pmap_wf t2 → Pmap_wf (merge f t1 t2).
 Proof. intros t1wf. revert t2. induction t1wf; destruct 1; simpl; auto. Qed.
-Global Instance Pmerge: Merge Pmap := λ A f t1 t2,
+Global Instance Pmerge {A} : Merge A (Pmap A) := λ f t1 t2,
   dexist (merge f (`t1) (`t2))
     (Pmerge_wf _ _ _ (proj2_dsig t1) (proj2_dsig t2)).
 
@@ -343,9 +371,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.
-    rewrite Plookup_raw_dom. unfold id. split.
-    + intros [? [??]]. by subst.
-    + naive_solver.
+  * intros ? [??]. apply Pto_list_raw_nodup.
+  * intros ? [??]. apply Pelem_of_to_list_raw.
   * intros ??? [??] [??] ?. by apply Pmerge_raw_spec.
 Qed.
diff --git a/theories/prelude.v b/theories/prelude.v
index 27ea3b2659e1f17888df9849378d743c51d7b08b..aa488b804e93688a7f929247d2ae4960f0ab0392 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -8,9 +8,9 @@ Require Export
   option
   vector
   numbers
+  ars
   collections
   fin_collections
   listset
-  listset_nodup
   fresh_numbers
   list.
diff --git a/theories/tactics.v b/theories/tactics.v
index 96d24a4114e1cb7fb08f5811e1ecd7e199cd121c..3f061096ddcfb80417893465bb0b74f2e7988ed0 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -36,6 +36,12 @@ Ltac done :=
 Tactic Notation "by" tactic(tac) :=
   tac; done.
 
+Ltac case_match :=
+  match goal with
+  | H : context [ match ?x with _ => _ end ] |- _ => destruct x eqn:?
+  | |- context [ match ?x with _ => _ end ] => destruct x eqn:?
+  end.
+
 (** The tactic [clear dependent H1 ... Hn] clears the hypotheses [Hi] and
 their dependencies. *)
 Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) :=
@@ -114,6 +120,8 @@ Ltac simplify_equality := repeat
   | H : ?x = _ |- _ => subst x
   | H : _ = ?x |- _ => subst x
   | H : _ = _ |- _ => discriminate H
+  | H : ?f _ = ?f _ |- _ => apply (injective f) in H
+    (* before [injection'] to circumvent bug #2939 in some situations *)
   | H : _ = _ |- _ => injection' H
   end.