From 18669b9259e8eacbf6dcaed25db562008ef3f13c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 Aug 2012 10:50:53 +0200
Subject: [PATCH] Major revision of the whole development.

The main changes are:

* Function calls in the operational semantics
* Mutually recursive function calls in the axiomatic semantics
* A general definition of the interpretation of the axiomatic semantics  so as
  to improve reusability (useful for function calls, and also for expressions
  in future versions)
* Type classes for stack independent, memory independent, and memory extensible
  assertions, and a lot of instances to automatically derive these properties.
* Many additional lemmas on the memory and more robust tactics to simplify
  goals involving is_free and mem_disjoint
* Proof of preservation of statements in the smallstep semantics

* Some new tactics: feed, feed destruct, feed inversion, etc...
* More robust tactic scripts using bullets and structured scripts
* Truncate most lines at 80 characters
---
 theories/base.v            | 190 ++++++++----
 theories/collections.v     | 103 +++++--
 theories/decidable.v       |  42 ++-
 theories/fin_collections.v | 144 ++++++----
 theories/fin_maps.v        | 572 ++++++++++++++++++++++++-------------
 theories/list.v            | 416 ++++++++++++++++++---------
 theories/listset.v         |  83 +++---
 theories/monads.v          |   3 +-
 theories/nmap.v            |  30 +-
 theories/numbers.v         |  19 +-
 theories/option.v          |  66 +++--
 theories/orders.v          |  29 +-
 theories/pmap.v            | 191 +++++++------
 theories/subset.v          |   4 +-
 theories/trs.v             |  58 +++-
 15 files changed, 1274 insertions(+), 676 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 23104556..b021a298 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -2,15 +2,14 @@ Global Generalizable All Variables.
 Global Set Automatic Coercions Import.
 Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid NArith.
 
-Arguments existT {_ _} _ _.
-Arguments existT2 {_ _ _} _ _ _.
+Arguments id _ _/.
+Arguments compose _ _ _ _ _ _ /.
+
+(* Change True and False into notations so we can overload them *)
+Notation "'True'" := True : type_scope.
+Notation "'False'" := False : type_scope.
 
-Definition proj1_T2 {A} {P Q : A → Type} (x : sigT2 P Q) : A :=
-  match x with existT2 a _ _ => a end.
-Definition proj2_T2 {A} {P Q : A → Type} (x : sigT2 P Q) : P (proj1_T2 x) :=
-  match x with existT2 _ p _ => p end.
-Definition proj3_T2 {A} {P Q : A → Type} (x : sigT2 P Q) : Q (proj1_T2 x) :=
-  match x with existT2 _ _ q => q end.
+Arguments existT {_ _} _ _.
 
 (*  Common notations *)
 Delimit Scope C_scope with C.
@@ -28,7 +27,8 @@ Hint Extern 0 (?x = ?x) => reflexivity.
 Notation "(→)" := (λ x y, x → y) : C_scope.
 Notation "( T →)" := (λ y, T → y) : C_scope.
 Notation "(→ T )" := (λ y, y → T) : C_scope.
-Notation "t $ r" := (t r) (at level 65, right associativity, only parsing) : C_scope.
+Notation "t $ r" := (t r)
+  (at level 65, right associativity,only parsing) : C_scope.
 Infix "∘" := compose : C_scope.
 Notation "(∘)" := compose (only parsing) : C_scope.
 Notation "( f ∘)" := (compose f) (only parsing) : C_scope.
@@ -91,8 +91,9 @@ Notation "( ⊈ X )" := (λ Y, Y ⊈ X) (only parsing) : C_scope.
 Hint Extern 0 (?x ⊆ ?x) => reflexivity.
 
 Class Singleton A B := singleton: A → B.
-Notation "{{ x }}" := (singleton x) : C_scope.
-Notation "{{ x ; y ; .. ; z }}" := (union .. (union (singleton x) (singleton y)) .. (singleton z)) : C_scope.
+Notation "{[ x ]}" := (singleton x) : C_scope.
+Notation "{[ x ; y ; .. ; z ]}" :=
+  (union .. (union (singleton x) (singleton y)) .. (singleton z)) : C_scope.
 
 Class ElemOf A B := elem_of: A → B → Prop.
 Infix "∈" := elem_of (at level 70) : C_scope.
@@ -104,16 +105,26 @@ Notation "(∉)" := (λ x X, x ∉ X) (only parsing) : C_scope.
 Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : C_scope.
 Notation "(∉ X )" := (λ x, x ∉ X) (only parsing) : C_scope.
 
-Class UnionWith M := union_with: ∀ {A}, (A → A → A) → M A → M A → M A.
-Class IntersectWith M := intersect_with: ∀ {A}, (A → A → A) → M A → M A → M A.
+Class UnionWith M :=
+  union_with: ∀ {A}, (A → A → A) → M A → M A → M A.
+Class IntersectionWith M :=
+  intersection_with: ∀ {A}, (A → A → A) → M A → M A → M A.
+Class DifferenceWith M :=
+  difference_with: ∀ {A}, (A → A → option A) → M A → M A → M A.
 
 (* Common properties *)
-Class Injective {A B} R S (f : A → B) := injective: ∀ x y : A, S (f x) (f y) → R x y.
-Class Idempotent {A} R (f : A → A → A) := idempotent: ∀ x, R (f x x) x.
-Class Commutative {A B} R (f : B → B → A) := commutative: ∀ x y, R (f x y) (f y x).
-Class LeftId {A} R (i : A) (f : A → A → A) := left_id: ∀ x, R (f i x) x.
-Class RightId {A} R (i : A) (f : A → A → A) := right_id: ∀ x, R (f x i) x.
-Class Associative {A} R (f : A → A → A) := associative: ∀ x y z, R (f x (f y z)) (f (f x y) z).
+Class Injective {A B} R S (f : A → B) :=
+  injective: ∀ x y : A, S (f x) (f y) → R x y.
+Class Idempotent {A} R (f : A → A → A) :=
+  idempotent: ∀ x, R (f x x) x.
+Class Commutative {A B} R (f : B → B → A) :=
+  commutative: ∀ x y, R (f x y) (f y x).
+Class LeftId {A} R (i : A) (f : A → A → A) :=
+  left_id: ∀ x, R (f i x) x.
+Class RightId {A} R (i : A) (f : A → A → A) :=
+  right_id: ∀ x, R (f x i) x.
+Class Associative {A} R (f : A → A → A) :=
+  associative: ∀ x y z, R (f x (f y z)) (f (f x y) z).
 
 Arguments injective {_ _ _ _} _ {_} _ _ _.
 Arguments idempotent {_ _} _ {_} _.
@@ -123,15 +134,20 @@ Arguments right_id {_ _} _ _ {_} _.
 Arguments associative {_ _} _ {_} _ _ _.
 
 (* Using idempotent_eq we can force Coq to not use the setoid mechanism *)
-Lemma idempotent_eq {A} (f : A → A → A) `{!Idempotent (=) f} x : f x x = x.
+Lemma idempotent_eq {A} (f : A → A → A) `{!Idempotent (=) f} x :
+  f x x = x.
 Proof. auto. Qed.
-Lemma commutative_eq {A B} (f : B → B → A) `{!Commutative (=) f} x y : f x y = f y x.
+Lemma commutative_eq {A B} (f : B → B → A) `{!Commutative (=) f} x y :
+  f x y = f y x.
 Proof. auto. Qed.
-Lemma left_id_eq {A} (i : A) (f : A → A → A) `{!LeftId (=) i f} x : f i x = x.
+Lemma left_id_eq {A} (i : A) (f : A → A → A) `{!LeftId (=) i f} x :
+  f i x = x.
 Proof. auto. Qed.
-Lemma right_id_eq {A} (i : A) (f : A → A → A) `{!RightId (=) i f} x : f x i = x.
+Lemma right_id_eq {A} (i : A) (f : A → A → A) `{!RightId (=) i f} x :
+  f x i = x.
 Proof. auto. Qed.
-Lemma associative_eq {A} (f : A → A → A) `{!Associative (=) f} x y z : f x (f y z) = f (f x y) z.
+Lemma associative_eq {A} (f : A → A → A) `{!Associative (=) f} x y z :
+  f x (f y z) = f (f x y) z.
 Proof. auto. Qed.
 
 (* Monadic operations *)
@@ -150,7 +166,8 @@ Arguments mjoin {M MJoin A} _.
 Arguments fmap {M FMap A B} _ _.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
-Notation "x ← y ; z" := (y ≫= (λ x : _, z)) (at level 65, next at level 35, right associativity) : C_scope.
+Notation "x ← y ; z" := (y ≫= (λ x : _, z))
+  (at level 65, next at level 35, right associativity) : C_scope.
 Infix "<$>" := fmap (at level 65, right associativity, only parsing) : C_scope.
 
 (* Ordered structures *)
@@ -159,7 +176,8 @@ Class BoundedPreOrder A `{Empty A} `{SubsetEq A} := {
   subseteq_empty x : ∅ ⊆ x
 }.
 
-(* Note: no equality to avoid the need for setoids. We define equality in a generic way. *)
+(* Note: no equality to avoid the need for setoids. We define setoid 
+equality in a generic way. *)
 Class BoundedJoinSemiLattice A `{Empty A} `{SubsetEq A} `{Union A} := {
   jsl_preorder :>> BoundedPreOrder A;
   subseteq_union_l x y : x ⊆ x ∪ y;
@@ -180,7 +198,7 @@ Class Map A C := map: (A → A) → (C → C).
 Class Collection A C `{ElemOf A C} `{Empty C} `{Union C} 
     `{Intersection C} `{Difference C} `{Singleton A C} `{Map A C} := {
   elem_of_empty (x : A) : x ∉ ∅;
-  elem_of_singleton (x y : A) : x ∈ {{ y }} ↔ x = y;
+  elem_of_singleton (x y : A) : x ∈ {[ y ]} ↔ x = y;
   elem_of_union X Y (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y;
   elem_of_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;
@@ -208,15 +226,31 @@ Notation "(!!)" := lookup (only parsing) : C_scope.
 Notation "( m !!)" := (λ i, lookup i m) (only parsing) : C_scope.
 Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
 
-Class PartialAlter K M := partial_alter: ∀ {A}, (option A → option A) → K → M A → M A.
-Class Alter K M := alter: ∀ {A}, (A → A) → K → M A → M A.
-Class Dom K M := dom: ∀ C `{Empty C} `{Union C} `{Singleton K C}, M → C.
-Class Merge M := merge: ∀ {A}, (option A → option A → option A) → M A → M A → M A.
-Class Insert K M := insert: ∀ {A}, K → A → M A → M A.
-Notation "<[ k := a ]>" := (insert k a) (at level 5, right associativity) : C_scope.
-Class Delete K M := delete: K → M → M.
+Class PartialAlter K M :=
+  partial_alter: ∀ {A}, (option A → option A) → K → M A → M A.
+Class Alter K M :=
+  alter: ∀ {A}, (A → A) → K → M A → M A.
+Class Dom K M :=
+  dom: ∀ C `{Empty C} `{Union C} `{Singleton K C}, M → C.
+Class Merge M :=
+  merge: ∀ {A}, (option A → option A → option A) → M A → M A → M A.
+Class Insert K M :=
+  insert: ∀ {A}, K → A → M A → M A.
+Notation "<[ k := a ]>" := (insert k a) 
+  (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
+Class Delete K M :=
+  delete: K → M → M.
+
+Definition insert_list `{Insert K M} {A} (l : list (K * A)) (m : M A) : M A :=
+  fold_right (λ p, <[ fst p := snd p ]>) m l.
+Definition delete_list `{Delete K M} (l : list K) (m : M) : M := 
+  fold_right delete m l.
 
 (* Misc *)
+Lemma symmetry_iff `(R : relation A) `{!Symmetric R} (x y : A) :
+  R x y ↔ R y x.
+Proof. intuition. Qed.
+
 Instance pointwise_reflexive {A} `{R : relation B} :
   Reflexive R → Reflexive (pointwise_relation A R) | 9.
 Proof. firstorder. Qed.
@@ -227,20 +261,26 @@ Instance pointwise_transitive {A} `{R : relation B} :
   Transitive R → Transitive (pointwise_relation A R) | 9.
 Proof. firstorder. Qed.
 
-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)).
-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).
+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)).
+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).
 
 Section prod_relation.
   Context `{R1 : relation A} `{R2 : relation B}.
-  Global Instance: Reflexive R1 → Reflexive R2 → Reflexive (prod_relation R1 R2).
+  Global Instance:
+    Reflexive R1 → Reflexive R2 → Reflexive (prod_relation R1 R2).
   Proof. firstorder eauto. Qed.
-  Global Instance: Symmetric R1 → Symmetric R2 → Symmetric (prod_relation R1 R2).
+  Global Instance:
+    Symmetric R1 → Symmetric R2 → Symmetric (prod_relation R1 R2).
   Proof. firstorder eauto. Qed.
-  Global Instance: Transitive R1 → Transitive R2 → Transitive (prod_relation R1 R2).
+  Global Instance:
+    Transitive R1 → Transitive R2 → Transitive (prod_relation R1 R2).
   Proof. firstorder eauto. Qed.
-  Global Instance: Equivalence R1 → Equivalence R2 → Equivalence (prod_relation R1 R2).
+  Global Instance:
+    Equivalence R1 → Equivalence R2 → Equivalence (prod_relation R1 R2).
   Proof. split; apply _. Qed.
   Global Instance: Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
   Proof. firstorder eauto. Qed.
@@ -250,11 +290,13 @@ Section prod_relation.
   Proof. firstorder eauto. Qed.
 End prod_relation.
 
-Definition lift_relation {A B} (R : relation A) (f : B → A) : relation B := λ x y, R (f x) (f y).
+Definition lift_relation {A B} (R : relation A)
+  (f : B → A) : relation B := λ x y, R (f x) (f y).
 Definition lift_relation_equivalence {A B} (R : relation A) (f : B → A) :
   Equivalence R → Equivalence (lift_relation R f).
 Proof. unfold lift_relation. firstorder. Qed.
-Hint Extern 0 (Equivalence (lift_relation _ _)) => eapply @lift_relation_equivalence : typeclass_instances.
+Hint Extern 0 (Equivalence (lift_relation _ _)) =>
+  eapply @lift_relation_equivalence : typeclass_instances.
 
 Instance: ∀ A B (x : B), Commutative (=) (λ _ _ : A, x).
 Proof. easy. Qed.
@@ -269,11 +311,14 @@ Proof. easy. Qed.
 Instance: ∀ A, Idempotent (=) (λ _ x : A, x).
 Proof. easy. Qed.
 
-Instance left_id_propholds {A} (R : relation A) i f : LeftId R i f → ∀ x, PropHolds (R (f i x) x).
+Instance left_id_propholds {A} (R : relation A) i f :
+  LeftId R i f → ∀ x, PropHolds (R (f i x) x).
 Proof. easy. Qed.
-Instance right_id_propholds {A} (R : relation A) i f : RightId R i f → ∀ x, PropHolds (R (f x i) x).
+Instance right_id_propholds {A} (R : relation A) i f :
+  RightId R i f → ∀ x, PropHolds (R (f x i) x).
 Proof. easy. Qed.
-Instance idem_propholds {A} (R : relation A) f : Idempotent R f → ∀ x, PropHolds (R (f x x) x).
+Instance idem_propholds {A} (R : relation A) f :
+  Idempotent R f → ∀ x, PropHolds (R (f x x) x).
 Proof. easy. Qed.
 
 Ltac simplify_eqs := repeat
@@ -283,7 +328,8 @@ Ltac simplify_eqs := repeat
   | H : _ ≠ _ |- _ => now destruct H
   | H : _ = _ → False |- _ => now destruct H
   | H : _ = _ |- _ => discriminate H
-  | H : _ = _ |-  ?G => change (id G); injection H; clear H; intros; unfold id at 1
+  | H : _ = _ |-  ?G =>
+    change (id G); injection H; clear H; intros; unfold id at 1
   | H : ?f _ = ?f _ |- _ => apply (injective f) in H
   | H : ?f _ ?x = ?f _ ?x |- _ => apply (injective (λ y, f y x)) in H
   end.
@@ -303,3 +349,51 @@ Tactic Notation "remember" constr(t) "as" "(" ident(x) "," ident(E) ")" :=
   match goal with
   | E' : x = _ |- _ => rename E' into E
   end.
+
+Ltac feed tac H :=
+  let H' := type of H in
+  match eval hnf in H' with
+  | ?T1 → ?T2 =>
+    let HT1 := fresh in assert T1 as HT1;
+    [| feed tac (H HT1); clear HT1 ]
+  | _ => tac H
+  end.
+Tactic Notation "feed" tactic(tac) constr(H) := feed tac H.
+
+Ltac efeed tac H :=
+  let H' := type of H in
+  match eval hnf in H' with
+  | ?T1 → ?T2 =>
+    let HT1 := fresh in assert T1 as HT1; [| efeed tac (H HT1); clear HT1 ]
+  | ?T1 → _ =>
+    let e := fresh in evar (e:T1);
+    let e' := eval unfold e in e in
+    clear e; efeed tac (H e')
+  | _ => tac H
+  end.
+Tactic Notation "efeed" tactic(tac) constr(H) := efeed tac H.
+
+Tactic Notation "feed" "pose" "proof" constr(H) "as" ident(H') :=
+  feed (fun H => pose proof H as H') H.
+Tactic Notation "feed" "pose" "proof" constr(H) :=
+  feed (fun H => pose proof H) H.
+
+Tactic Notation "efeed" "pose" "proof" constr(H) "as" ident(H') :=
+  efeed (fun H => pose proof H as H') H.
+Tactic Notation "efeed" "pose" "proof" constr(H) :=
+  efeed (fun H => pose proof H) H.
+
+Tactic Notation "feed" "specialize" ident(H) :=
+  feed (fun H => specialize H) H.
+Tactic Notation "efeed" "specialize" ident(H) :=
+  efeed (fun H => specialize H) H.
+
+Tactic Notation "feed" "inversion" constr(H) :=
+  feed (fun H => let H':=fresh in pose proof H as H'; inversion H') H.
+Tactic Notation "feed" "inversion" constr(H) "as" simple_intropattern(IP) :=
+  feed (fun H => let H':=fresh in pose proof H as H'; inversion H' as IP) H.
+
+Tactic Notation "feed" "destruct" constr(H) :=
+  feed (fun H => let H':=fresh in pose proof H as H'; destruct H') H.
+Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
+  feed (fun H => let H':=fresh in pose proof H as H'; destruct H' as IP) H.
diff --git a/theories/collections.v b/theories/collections.v
index e2cd1d43..d7e107ef 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -21,28 +21,36 @@ Section collection.
   Proof. easy. Qed.
   Lemma elem_of_equiv X Y : X ≡ Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
   Proof. firstorder. Qed.
-  Lemma elem_of_equiv_alt X Y : X ≡ Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ (∀ x, x ∈ Y → x ∈ X).
+  Lemma elem_of_equiv_alt X Y :
+    X ≡ Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ (∀ x, x ∈ Y → x ∈ X).
   Proof. firstorder. Qed.
 
   Global Instance: Proper ((=) ==> (≡) ==> iff) (∈).
   Proof. intros ???. subst. firstorder. Qed.
 
-  Lemma empty_ne_singleton x :  ∅ ≢ {{ x }}.
-  Proof. intros [_ E]. destruct (elem_of_empty x). apply E. now apply elem_of_singleton. Qed. 
+  Lemma empty_ne_singleton x :  ∅ ≢ {[ x ]}.
+  Proof.
+    intros [_ E]. destruct (elem_of_empty x).
+    apply E. now apply elem_of_singleton.
+  Qed. 
 End collection.
 
 Section cmap.
   Context `{Collection A C}.
 
-  Lemma elem_of_map_1 (f : A → A) (X : C) (x : A) : x ∈ X → f x ∈ map f X.
+  Lemma elem_of_map_1 (f : A → A) (X : C) (x : A) :
+    x ∈ X → f x ∈ map f X.
   Proof. intros. apply (elem_of_map _). eauto. Qed.
-  Lemma elem_of_map_1_alt (f : A → A) (X : C) (x : A) y : x ∈ X → y = f x → y ∈ map f X.
+  Lemma elem_of_map_1_alt (f : A → A) (X : C) (x : A) y :
+    x ∈ X → y = f x → y ∈ map f X.
   Proof. intros. apply (elem_of_map _). eauto. Qed.
-  Lemma elem_of_map_2 (f : A → A) (X : C) (x : A) : x ∈ map f X → ∃ y, x = f y ∧ y ∈ X.
+  Lemma elem_of_map_2 (f : A → A) (X : C) (x : A) :
+    x ∈ map f X → ∃ y, x = f y ∧ y ∈ X.
   Proof. intros. now apply (elem_of_map _). Qed.
 End cmap.
 
-Definition fresh_sig `{FreshSpec A C} (X : C) : { x : A | x ∉ X } := exist (∉ X) (fresh X) (is_fresh X).
+Definition fresh_sig `{FreshSpec A C} (X : C) : { x : A | x ∉ X } :=
+  exist (∉ X) (fresh X) (is_fresh X).
 
 Lemma elem_of_fresh_iff `{FreshSpec A C} (X : C) : fresh X ∈ X ↔ False.
 Proof. split. apply is_fresh. easy. Qed.
@@ -52,7 +60,7 @@ Ltac split_elem_ofs := repeat
   | H : context [ _ ⊆ _ ] |- _ => setoid_rewrite elem_of_subseteq in H
   | H : context [ _ ≡ _ ] |- _ => setoid_rewrite elem_of_equiv_alt in H
   | H : context [ _ ∈ ∅ ] |- _ => setoid_rewrite elem_of_empty_iff in H
-  | H : context [ _ ∈ {{ _ }} ] |- _ => setoid_rewrite elem_of_singleton in H
+  | H : context [ _ ∈ {[ _ ]} ] |- _ => setoid_rewrite elem_of_singleton in H
   | H : context [ _ ∈ _ ∪ _ ] |- _ => setoid_rewrite elem_of_union in H
   | H : context [ _ ∈ _ ∩ _ ] |- _ => setoid_rewrite elem_of_intersection in H
   | H : context [ _ ∈ _ ∖ _ ] |- _ => setoid_rewrite elem_of_difference in H
@@ -60,7 +68,7 @@ Ltac split_elem_ofs := repeat
   | |- context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq
   | |- context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt
   | |- context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty_iff
-  | |- context [ _ ∈ {{ _ }} ] => setoid_rewrite elem_of_singleton
+  | |- context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton
   | |- context [ _ ∈ _ ∪ _ ] => setoid_rewrite elem_of_union
   | |- context [ _ ∈ _ ∩ _ ] => setoid_rewrite elem_of_intersection
   | |- context [ _ ∈ _ ∖ _ ] => setoid_rewrite elem_of_difference
@@ -97,9 +105,12 @@ Ltac naive_firstorder t :=
   (* solve *)
   | |- _ => solve [t]
   (* dirty destructs *)
-  | H : context [ ∃ _, _ ] |- _ => edestruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
-  | H : context [ _ ∧ _ ] |- _ => edestruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
-  | H : context [ _ ∨ _ ] |- _ => edestruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
+  | H : context [ ∃ _, _ ] |- _ =>
+    edestruct H; clear H;naive_firstorder t || clear H; naive_firstorder t
+  | H : context [ _ ∧ _ ] |- _ => 
+    destruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
+  | H : context [ _ ∨ _ ] |- _ =>
+    edestruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
   (* dirty constructs *)
   | |- ∃ x, _ => eexists; naive_firstorder t
   | |- _ ∨ _ => left; naive_firstorder t || right; naive_firstorder t
@@ -125,8 +136,8 @@ Section no_dup.
   Global Instance: Proper (R ==> (≡) ==> iff) elem_of_upto.
   Proof.
     intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
-     rewrite <-E1, <-E2; intuition.
-    rewrite E1, E2; intuition.
+    * rewrite <-E1, <-E2; intuition.
+    * rewrite E1, E2; intuition.
   Qed.
   Global Instance: Proper ((≡) ==> iff) no_dup.
   Proof. firstorder. Qed.
@@ -135,20 +146,24 @@ Section no_dup.
   Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
   Lemma elem_of_upto_empty x : ¬elem_of_upto x ∅.
   Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
-  Lemma elem_of_upto_singleton x y : elem_of_upto x {{ y }} ↔ R x y.
+  Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} ↔ R x y.
   Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
 
-  Lemma elem_of_upto_union X Y x : elem_of_upto x (X ∪ Y) ↔ elem_of_upto x X ∨ elem_of_upto x Y.
+  Lemma elem_of_upto_union X Y x :
+    elem_of_upto x (X ∪ Y) ↔ elem_of_upto x X ∨ elem_of_upto x Y.
   Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
   Lemma not_elem_of_upto x X : ¬elem_of_upto x X → ∀ y, y ∈ X → ¬R x y.
   Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
 
   Lemma no_dup_empty: no_dup ∅.
   Proof. unfold no_dup. simplify_elem_of. Qed.
-  Lemma no_dup_add x X : ¬elem_of_upto x X → no_dup X → no_dup ({{ x }} ∪ X).
+  Lemma no_dup_add x X : ¬elem_of_upto x X → no_dup X → no_dup ({[ x ]} ∪ X).
   Proof. unfold no_dup, elem_of_upto. esimplify_elem_of. Qed.
-  Lemma no_dup_inv_add x X : x ∉ X → no_dup ({{ x }} ∪ X) → ¬elem_of_upto x X.
-  Proof. intros Hin Hnodup [y [??]]. rewrite (Hnodup x y) in Hin; simplify_elem_of. Qed.
+  Lemma no_dup_inv_add x X : x ∉ X → no_dup ({[ x ]} ∪ X) → ¬elem_of_upto x X.
+  Proof.
+    intros Hin Hnodup [y [??]].
+    rewrite (Hnodup x y) in Hin; simplify_elem_of.
+  Qed.
   Lemma no_dup_inv_union_l X Y : no_dup (X ∪ Y) → no_dup X.
   Proof. unfold no_dup. simplify_elem_of. Qed.
   Lemma no_dup_inv_union_r X Y : no_dup (X ∪ Y) → no_dup Y.
@@ -163,7 +178,7 @@ Section quantifiers.
 
   Lemma cforall_empty : cforall ∅.
   Proof. unfold cforall. simplify_elem_of. Qed.
-  Lemma cforall_singleton x : cforall {{ x }} ↔ P x.
+  Lemma cforall_singleton x : cforall {[ x ]} ↔ P x.
   Proof. unfold cforall. simplify_elem_of. Qed.
   Lemma cforall_union X Y : cforall X → cforall Y → cforall (X ∪ Y).
   Proof. unfold cforall. simplify_elem_of. Qed.
@@ -174,7 +189,7 @@ Section quantifiers.
 
   Lemma cexists_empty : ¬cexists ∅.
   Proof. unfold cexists. esimplify_elem_of. Qed.
-  Lemma cexists_singleton x : cexists {{ x }} ↔ P x.
+  Lemma cexists_singleton x : cexists {[ x ]} ↔ P x.
   Proof. unfold cexists. esimplify_elem_of. Qed.
   Lemma cexists_union_1 X Y : cexists X → cexists (X ∪ Y).
   Proof. unfold cexists. esimplify_elem_of. Qed.
@@ -184,9 +199,43 @@ Section quantifiers.
   Proof. unfold cexists. esimplify_elem_of. Qed.
 End quantifiers.
 
-Lemma cforall_weak `{Collection A B} (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X :
-  cforall P X → cforall Q X.
-Proof. firstorder. Qed.
-Lemma cexists_weak `{Collection A B} (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X :
-  cexists P X → cexists Q X.
-Proof. firstorder. Qed.
+Section more_quantifiers.
+  Context `{Collection A B}.
+  
+  Lemma cforall_weak (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X :
+    cforall P X → cforall Q X.
+  Proof. firstorder. Qed.
+  Lemma cexists_weak (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X :
+    cexists P X → cexists Q X.
+  Proof. firstorder. Qed.
+End more_quantifiers.
+
+Section fresh.
+  Context `{Collection A C} `{Fresh A C} `{!FreshSpec A C} .
+
+  Fixpoint fresh_list (n : nat) (X : C) : list A :=
+    match n with
+    | 0 => []
+    | S n => let x := fresh X in x :: fresh_list n ({[ x ]} ∪ X)
+    end.
+
+  Lemma fresh_list_length n X : length (fresh_list n X) = n.
+  Proof. revert X. induction n; simpl; auto. Qed.
+
+  Lemma fresh_list_is_fresh n X x : In x (fresh_list n X) → x ∉ X.
+  Proof.
+    revert X. induction n; simpl.
+    * easy.
+    * intros X [?| Hin]. subst.
+      + apply is_fresh.
+      + apply IHn in Hin. simplify_elem_of.
+  Qed.
+
+  Lemma fresh_list_nodup n X : NoDup (fresh_list n X).
+  Proof.
+    revert X.
+    induction n; simpl; constructor; auto.
+    intros Hin. apply fresh_list_is_fresh in Hin.
+    simplify_elem_of.
+  Qed.
+End fresh.
diff --git a/theories/decidable.v b/theories/decidable.v
index 4c0b72c8..3cbb7124 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -6,9 +6,11 @@ Definition decide_rel {A B} (R : A → B → Prop)
 Ltac case_decide := 
   match goal with
   | H : context [@decide ?P ?dec] |- _ => case (@decide P dec) in *
-  | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ => case (@decide_rel _ _ R x y dec) in *
+  | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ =>
+     case (@decide_rel _ _ R x y dec) in *
   | |- context [@decide ?P ?dec] => case (@decide P dec) in *
-  | |- context [@decide_rel _ _ ?R ?x ?y ?dec] => case (@decide_rel _ _ R x y dec) in *
+  | |- context [@decide_rel _ _ ?R ?x ?y ?dec] =>
+     case (@decide_rel _ _ R x y dec) in *
   end.
 
 Ltac solve_trivial_decision :=
@@ -16,25 +18,28 @@ Ltac solve_trivial_decision :=
   | [ |- Decision (?P) ] => apply _
   | [ |- sumbool ?P (¬?P) ] => change (Decision P); apply _
   end.
-Ltac solve_decision :=
-  first [solve_trivial_decision | unfold Decision; decide equality; solve_trivial_decision].
+Ltac solve_decision := 
+  intros; first [ solve_trivial_decision
+                | unfold Decision; decide equality; solve_trivial_decision ].
 
 Program Instance True_dec: Decision True := left _.
 Program Instance False_dec: Decision False := right _.
 Program 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) := λ x y,
+    `(B_dec : ∀ x y : B, Decision (x = y)) : ∀ x y : A * B, Decision (x = y) := λ x y,
   match A_dec (fst x) (fst y) with
   | left _ => match B_dec (snd x) (snd y) with left _ => left _ | right _ => right _ end
   | right _ => right _
   end.
 Solve Obligations using (program_simpl; f_equal; firstorder).
-Program Instance and_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ∧ Q) :=
+Program Instance and_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
+    Decision (P ∧ Q) :=
   match P_dec with
   | left _ => match Q_dec with left _ => left _ | right _ => right _ end
   | right _ => right _
   end.
 Solve Obligations using (program_simpl; tauto).
-Program Instance or_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ∨ Q) :=
+Program Instance or_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
+    Decision (P ∨ Q) :=
   match P_dec with
   | left _ => left _
   | right _ => match Q_dec with left _ => left _ | right _ => right _ end
@@ -48,15 +53,22 @@ Proof. unfold bool_decide. now destruct dec. Qed.
 Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
 Proof. unfold bool_decide. now destruct dec. Qed.
 
-Definition dsig `(P : A → Prop) `{∀ x : A, Decision (P x)} := { x | bool_decide (P x) }.
-Definition proj2_dsig `{∀ x : A, Decision (P x)} (x : dsig P) : P (`x) := bool_decide_unpack _ (proj2_sig x).
-Definition dexist `{∀ x : A, Decision (P x)} (x : A) (p : P x) : dsig P := x↾bool_decide_pack _ p.
+Definition dsig `(P : A → Prop) `{∀ x : A, Decision (P x)} :=
+  { x | bool_decide (P x) }.
+Definition proj2_dsig `{∀ x : A, Decision (P x)} (x : dsig P) : P (`x) :=
+  bool_decide_unpack _ (proj2_sig x).
+Definition dexist `{∀ x : A, Decision (P x)} (x : A) (p : P x) : dsig P :=
+  x↾bool_decide_pack _ p.
 
-Lemma proj1_dsig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) : x↾Px = y↾Py → x = y.
+Lemma proj1_dsig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) :
+  x↾Px = y↾Py → x = y.
 Proof. now injection 1. Qed.
-Lemma dsig_eq {A} (P : A → Prop) {dec : ∀ x, Decision (P x)} (x y : { x | bool_decide (P x) }) :
-  `x = `y → x = y.
+Lemma dsig_eq {A} (P : A → Prop) {dec : ∀ x, Decision (P x)}
+  (x y : { x | bool_decide (P x) }) : `x = `y → x = y.
 Proof.
-  intros H1. destruct x as [x Hx], y as [y Hy]. simpl in *. subst.
-  f_equal. revert Hx Hy. case (bool_decide (P y)). simpl. now intros [] []. easy.
+  intros H1. destruct x as [x Hx], y as [y Hy].
+  simpl in *. subst. f_equal.
+  revert Hx Hy. case (bool_decide (P y)).
+  * now intros [] [].
+  * easy.
 Qed.
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 8e39d4d5..f823d7c5 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -11,9 +11,9 @@ Context `{FinCollection A C}.
 Global Instance elements_proper: Proper ((≡) ==> Permutation) elements.
 Proof.
   intros ?? E. apply NoDup_Permutation.
-    apply elements_nodup.
-   apply elements_nodup.
-  intros. now rewrite <-!elements_spec, E.
+  * apply elements_nodup.
+  * apply elements_nodup.
+  * intros. now rewrite <-!elements_spec, E.
 Qed.
 Global Instance collection_size_proper: Proper ((≡) ==> (=)) size.
 Proof. intros ?? E. apply Permutation_length. now rewrite E. Qed.
@@ -21,8 +21,8 @@ Proof. intros ?? E. apply Permutation_length. now rewrite E. Qed.
 Lemma size_empty : size ∅ = 0.
 Proof.
   unfold size, collection_size. rewrite (in_nil_inv (elements ∅)).
-   easy.
-  intro. rewrite <-elements_spec. simplify_elem_of.
+  * easy.
+  * intro. rewrite <-elements_spec. simplify_elem_of.
 Qed.
 Lemma size_empty_inv X : size X = 0 → X ≡ ∅.
 Proof.
@@ -32,52 +32,54 @@ Qed.
 Lemma size_empty_iff X : size X = 0 ↔ X ≡ ∅.
 Proof. split. apply size_empty_inv. intros E. now rewrite E, size_empty. Qed.
 
-Lemma size_singleton x : size {{ x }} = 1.
+Lemma size_singleton x : size {[ x ]} = 1.
 Proof.
-  change (length (elements {{x}}) = length [x]).
+  change (length (elements {[ x ]}) = length [x]).
   apply Permutation_length, NoDup_Permutation.
-    apply elements_nodup.
-   apply NoDup_singleton.
-  intros. rewrite <-elements_spec. esimplify_elem_of firstorder.
+  * apply elements_nodup.
+  * apply NoDup_singleton.
+  * intros. rewrite <-elements_spec. esimplify_elem_of firstorder.
 Qed.
 Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
 Proof.
   unfold size, collection_size. rewrite !elements_spec.
   generalize (elements X). intros [|? l].
-   discriminate.
-  injection 1. intro. rewrite (nil_length l) by easy.
-  simpl. intuition congruence.
+  * discriminate.
+  * injection 1. intro. rewrite (nil_length l) by easy.
+    simpl. intuition congruence.
 Qed.
 
 Lemma choose X : X ≢ ∅ → { x | x ∈ X }.
 Proof.
   case_eq (elements X).
-   intros E. intros []. apply equiv_empty.
-   intros x. rewrite elements_spec, E. contradiction.
-  intros x l E. exists x. rewrite elements_spec, E. now left.
+  * intros E. intros []. apply equiv_empty.
+    intros x. rewrite elements_spec, E. contradiction.
+  * intros x l E. exists x.
+    rewrite elements_spec, E. now left.
 Qed.
 Lemma size_pos_choose X : 0 < size X → { x | x ∈ X }.
 Proof. 
   intros E. apply choose.
-  intros E2. rewrite E2, size_empty in E. now destruct (Lt.lt_n_0 0).
+  intros E2. rewrite E2, size_empty in E.
+  now destruct (Lt.lt_n_0 0).
 Qed.
-Lemma size_1_choose X : size X = 1 → { x | X ≡ {{ x }} }.
+Lemma size_1_choose X : size X = 1 → { x | X ≡ {[ x ]} }.
 Proof.
   intros E. destruct (size_pos_choose X).
-   rewrite E. auto with arith.
-  exists x. simplify_elem_of. eapply size_singleton_inv; eauto.
+  * rewrite E. auto with arith.
+  * exists x. simplify_elem_of. eapply size_singleton_inv; eauto.
 Qed.
 
 Program Instance collection_car_eq_dec_slow (x y : A) : Decision (x = y) | 100 :=
-  match Compare_dec.zerop (size ({{ x }} ∩ {{ y }})) with
+  match Compare_dec.zerop (size ({[ x ]} ∩ {[ y ]})) with
   | left _ => right _
   | right _ => left _
   end.
 Next Obligation.
   intro. apply empty_ne_singleton with x.
-  transitivity ({{ x }} ∩ {{ y }}).
-   symmetry. now apply size_empty_iff.
-  simplify_elem_of.
+  transitivity ({[ x ]} ∩ {[ y ]}).
+  * symmetry. now apply size_empty_iff.
+  * simplify_elem_of.
 Qed.
 Next Obligation. edestruct size_pos_choose; esimplify_elem_of. Qed.
 
@@ -87,9 +89,7 @@ Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100 :=
   | right Hx => right (Hx ∘ proj1 (elements_spec _ _))
   end.
 
-Lemma union_diff_1 X Y : X ⊆ Y → X ∪ Y ∖ X ≡ Y.
-Proof. split; intros x; destruct (decide (x ∈ X)); simplify_elem_of. Qed.
-Lemma union_diff_2 X Y : X ∪ Y ≡ X ∪ Y ∖ X.
+Lemma union_difference X Y : X ∪ Y ∖ X ≡ X ∪ Y.
 Proof. split; intros x; destruct (decide (x ∈ X)); simplify_elem_of. Qed.
 
 Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y.
@@ -103,80 +103,98 @@ Proof.
   intros. rewrite in_app_iff, <-!elements_spec. simplify_elem_of.
 Qed.
 Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
-Proof. rewrite <-size_union. now rewrite union_diff_2. simplify_elem_of. Qed.
-Lemma size_add X x : x ∉ X → size ({{ x }} ∪ X) = S (size X).
+Proof. rewrite <-size_union. now rewrite union_difference. simplify_elem_of. Qed.
+Lemma size_add X x : x ∉ X → size ({[ x ]} ∪ X) = S (size X).
 Proof. intros. rewrite size_union. now rewrite size_singleton. simplify_elem_of. Qed.
-Lemma size_diff X Y : X ⊆ Y → size X + size (Y ∖ X) = size Y.
+Lemma size_difference X Y : X ⊆ Y → size X + size (Y ∖ X) = size Y.
 Proof. intros. now rewrite <-size_union_alt, subseteq_union_1. Qed.
-Lemma size_remove X x : x ∈ X → S (size (X ∖ {{ x }})) = size X.
+Lemma size_remove X x : x ∈ X → S (size (X ∖ {[ x ]})) = size X.
 Proof.
-  intros. rewrite <-(size_diff {{ x }} X).
-   rewrite size_singleton. auto with arith.
-  simplify_elem_of.
+  intros. rewrite <-(size_difference {[ x ]} X).
+  * rewrite size_singleton. auto with arith.
+  * simplify_elem_of.
 Qed.
 
 Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
-Proof. intros. rewrite <-(union_diff_1 X Y), size_union by simplify_elem_of. auto with arith. Qed. 
+Proof.
+  intros. rewrite <-(subseteq_union_1 X Y) by easy.
+  rewrite <-(union_difference X Y), size_union by simplify_elem_of.
+  auto with arith.
+Qed. 
 
 Lemma collection_wf_ind (P : C → Prop) :
   (∀ X, (∀ Y, size Y < size X → P Y) → P X) → ∀ X, P X.
 Proof.
-  intros Hind. assert (∀ n X, size X < n → P X) as help.
-   induction n.
-    intros. now destruct (Lt.lt_n_0 (size X)).
-   intros. apply Hind. intros. apply IHn. eauto with arith.
-  intros. apply help with (S (size X)). auto with arith.
+  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.
+  * now destruct (Lt.lt_n_0 (size X)).
+  * apply Hind. intros. apply IHn. eauto with arith.
 Qed.
 
 Lemma collection_ind (P : C → Prop) :
-  Proper ((≡) ==> iff) P → P ∅ → (∀ x X, x ∉ X → P X → P ({{ x }} ∪ X)) → ∀ X, P X.
+  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)).
-   now rewrite size_empty_inv.
-  destruct (size_pos_choose X); auto.
-  rewrite <-(union_diff_1 {{ x }} X); simplify_elem_of.
-  apply Hadd; simplify_elem_of. apply IH.
-  rewrite <-(size_remove X x); auto with arith.
+  * now rewrite size_empty_inv.
+  * destruct (size_pos_choose X); auto.
+    rewrite <-(subseteq_union_1 {[ x ]} X) by simplify_elem_of.
+    rewrite <-union_difference.
+    apply Hadd; simplify_elem_of. apply IH.
+    rewrite <-(size_remove X x); auto with arith.
 Qed.
 
 Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
   Proper ((=) ==> (≡) ==> iff) P →
-  P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({{ x }} ∪ X)) → ∀ X, P (collection_fold f b X) X.
+  P b ∅ →
+  (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
+  ∀ X, P (collection_fold f b X) X.
 Proof.
   intros ? Hemp Hadd.
-  assert (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ In x l) → P (fold_right f b l) X) as help.
-   induction 1 as [|x l ?? IHl]; simpl.
-    intros X HX. rewrite equiv_empty; esimplify_elem_of.
-   intros X HX. rewrite <-(union_diff_1 {{ x }} X).
+  cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ In x l) → P (fold_right f b l) X).
+  { intros help ?. apply help. apply elements_nodup. apply elements_spec. }
+  induction 1 as [|x l ?? IHl]; simpl.
+  * intros X HX. rewrite equiv_empty. easy. intros ??. firstorder.
+  * intros X HX.
+    rewrite <-(subseteq_union_1 {[ x ]} X) by esimplify_elem_of.
+    rewrite <-union_difference.
     apply Hadd. simplify_elem_of. apply IHl.
     intros y. split.
-     intros. destruct (proj1 (HX y)); simplify_elem_of.
-    esimplify_elem_of.
-   esimplify_elem_of.
-  intros. apply help. apply elements_nodup. apply elements_spec.
+    + intros. destruct (proj1 (HX y)); simplify_elem_of.
+    + esimplify_elem_of.
 Qed.
 
 Lemma collection_fold_proper {B} (f : A → B → B) (b : B) :
   (∀ a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) → Proper ((≡) ==> (=)) (collection_fold f b).
 Proof. intros ??? E. apply fold_right_permutation. auto. now rewrite E. Qed. 
 
-Global Program Instance cforall_dec `(P : A → Prop) `{∀ x, Decision (P x)} X : Decision (cforall P X) | 100 :=
+Global Program Instance cforall_dec `(P : A → Prop)
+    `{∀ x, Decision (P x)} X : Decision (cforall P X) | 100 :=
   match decide (Forall P (elements X)) with
   | left Hall => left _
   | right Hall => right _
   end.
-Next Obligation. red. setoid_rewrite elements_spec. now apply Forall_forall. Qed. 
-Next Obligation. intro. apply Hall, Forall_forall. setoid_rewrite <-elements_spec. auto. Qed.
+Next Obligation.
+  red. setoid_rewrite elements_spec. now apply Forall_forall.
+Qed. 
+Next Obligation.
+  intro. apply Hall, Forall_forall. setoid_rewrite <-elements_spec. auto.
+Qed.
 
-Global Program Instance cexists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X : Decision (cexists P X) | 100 :=
+Global Program Instance cexists_dec `(P : A → Prop)
+    `{∀ x, Decision (P x)} X : Decision (cexists P X) | 100 :=
   match decide (Exists P (elements X)) with
   | left Hex => left _
   | right Hex => right _
   end.
-Next Obligation. red. setoid_rewrite elements_spec. now apply Exists_exists. Qed. 
-Next Obligation. intro. apply Hex, Exists_exists. setoid_rewrite <-elements_spec. auto. Qed.
+Next Obligation.
+  red. setoid_rewrite elements_spec. now apply Exists_exists. 
+Qed. 
+Next Obligation.
+  intro. apply Hex, Exists_exists. setoid_rewrite <-elements_spec. auto.
+Qed.
 
-Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X : Decision (elem_of_upto R x X) | 100 := 
-  decide (cexists (R x) X).
+Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X :
+  Decision (elem_of_upto R x X) | 100 := decide (cexists (R x) X).
 End fin_collection.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index b85be1f3..f9a755a8 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2,230 +2,400 @@ Require Export prelude.
 
 Class FinMap K M `{∀ A, Empty (M A)} `{Lookup K M} `{FMap M} 
     `{PartialAlter K M} `{∀ A, Dom K (M A)} `{Merge M} := {
-  finmap_eq {A} (m1 m2 : M A) : (∀ i, m1 !! i = m2 !! i) → m1 = m2;
-  lookup_empty {A} i : (∅ : M A) !! i = None;
-  lookup_partial_alter {A} f (m : M A) i : partial_alter f i m !! i = f (m !! i);
-  lookup_partial_alter_ne {A} f (m : M A) i j : 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_eq {A} (m1 m2 : M A) :
+    (∀ i, m1 !! i = m2 !! i) → m1 = m2;
+  lookup_empty {A} i :
+    (∅ : M A) !! i = None;
+  lookup_partial_alter {A} f (m : M A) i :
+    partial_alter f i m !! i = f (m !! i);
+  lookup_partial_alter_ne {A} f (m : M A) i j :
+    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);
   merge_spec {A} f `{!PropHolds (f None None = None)} 
     (m1 m2 : M A) i : merge f m1 m2 !! i = f (m1 !! i) (m2 !! i)
 }.
 
-Instance finmap_alter `{PartialAlter K M} : Alter K M := λ A f, partial_alter (fmap f).
-Instance finmap_insert `{PartialAlter K M} : Insert K M := λ A k x, partial_alter (λ _, Some x) k.
-Instance finmap_delete `{PartialAlter K M} {A} : Delete K (M A) := partial_alter (λ _, None).
-Instance finmap_singleton `{PartialAlter K M} {A} `{Empty (M A)} : Singleton (K * A) (M A) := λ p,
-  partial_alter (λ _, Some (snd p)) (fst p) ∅.
+Instance finmap_alter `{PartialAlter K M} : Alter K M := λ A f,
+  partial_alter (fmap f).
+Instance finmap_insert `{PartialAlter K M} : Insert K M := λ A k x,
+  partial_alter (λ _, Some x) k.
+Instance finmap_delete `{PartialAlter K M} {A} : Delete K (M A) :=
+  partial_alter (λ _, None).
+Instance finmap_singleton `{PartialAlter K M} {A} 
+  `{Empty (M A)} : Singleton (K * A) (M A) := λ p, <[fst p:=snd p]>∅.
 
-Definition insert_list `{Insert K M} {A} (l : list (K * A)) (m : M A) : M A := fold_right (λ p, <[ fst p := snd p ]>) m l.
+Definition list_to_map `{Insert K M} {A} `{Empty (M A)} (l : list (K * A)) : M A :=
+  insert_list l ∅.
 
-Instance finmap_union `{Merge M} : UnionWith M := λ A f, merge (union_with f).
-Instance finmap_intersect `{Merge M} : IntersectWith M := λ A f, merge (intersect_with f).
+Instance finmap_union `{Merge M} : UnionWith M := λ A f,
+  merge (union_with f).
+Instance finmap_intersection `{Merge M} : IntersectionWith M := λ A f,
+  merge (intersection_with f).
+Instance finmap_difference `{Merge M} : DifferenceWith M := λ A f,
+  merge (difference_with f).
 
 Section finmap.
-  Context `{FinMap K M} `{∀ i j : K, Decision (i = j)} {A : Type}.
-
-  Global Instance finmap_subseteq: SubsetEq (M A) := λ m n, ∀ i x, m !! i = Some x → n !! i = Some x.
-  Global Instance: BoundedPreOrder (M A).
-  Proof. split. firstorder. intros m i x. rewrite lookup_empty. discriminate. Qed.
-
-  Lemma not_elem_of_dom C `{Collection K C} (m : M A) i : i ∉ dom C m ↔ m !! i = None.
-  Proof. now 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. now 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. simplify_is_Some. simplify_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. simplify_elem_of. Qed.
-
-  Lemma lookup_empty_not i : ¬is_Some ((∅ : M A) !! i).
-  Proof. rewrite lookup_empty. simplify_is_Some. Qed.
-  Lemma lookup_empty_Some i (x : A) : ¬∅ !! i = Some x.
-  Proof. rewrite lookup_empty. discriminate. Qed.
-
-  Lemma lookup_singleton i (x : A) : {{ (i, x) }} !! i = Some x.
-  Proof. unfold singleton, finmap_singleton. apply lookup_partial_alter. Qed.
-  Lemma lookup_singleton_ne i j (x : A) : i ≠ j → {{ (i, x) }} !! j = None.
-  Proof.
-    unfold singleton, finmap_singleton.
-    intros. rewrite <-(lookup_empty j). now apply lookup_partial_alter_ne.
-  Qed.
-  Lemma lookup_ne (m : M A) i j : m !! i ≠ m !! j → i ≠ j.
-  Proof. congruence. Qed.
+Context `{FinMap K M} `{∀ i j : K, Decision (i = j)} {A : Type}.
+
+Global Instance finmap_subseteq: SubsetEq (M A) := λ m n,
+  ∀ i x, m !! i = Some x → n !! i = Some x.
+Global Instance: BoundedPreOrder (M A).
+Proof. split. firstorder. intros m i x. rewrite lookup_empty. discriminate. Qed.
+
+Lemma lookup_subseteq_Some (m1 m2 : M A) i x :
+  m1 ⊆ m2 → m1 !! i = Some x → m2 !! i = Some x.
+Proof. auto. Qed.
+Lemma lookup_subseteq_None (m1 m2 : M A) i :
+  m1 ⊆ m2 → m2 !! i = None → m1 !! i = None.
+Proof. rewrite !eq_None_not_Some. firstorder. Qed.
+Lemma lookup_ne (m : M A) i j : m !! i ≠ m !! j → i ≠ j.
+Proof. congruence. Qed.
+
+Lemma not_elem_of_dom C `{Collection K C} (m : M A) i :
+  i ∉ dom C m ↔ m !! i = None.
+Proof. now 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. now 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. simplify_is_Some.
+  * simplify_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. simplify_elem_of.
+Qed.
+
+Lemma lookup_empty_not i : ¬is_Some ((∅ : M A) !! i).
+Proof. rewrite lookup_empty. simplify_is_Some. Qed.
+Lemma lookup_empty_Some i (x : A) : ¬∅ !! i = Some x.
+Proof. rewrite lookup_empty. discriminate. Qed.
+
+Lemma partial_alter_compose (m : M A) i f g :
+  partial_alter (f ∘ g) i m = partial_alter f i (partial_alter g i m).
+Proof.
+  intros. apply finmap_eq. intros ii. case (decide (i = ii)).
+  * intros. subst. now rewrite !lookup_partial_alter.
+  * intros. now rewrite !lookup_partial_alter_ne.
+Qed.
+Lemma partial_alter_comm (m : M A) i j f g :
+  i ≠ j →
+ partial_alter f i (partial_alter g j m) = partial_alter g j (partial_alter f i m).
+Proof.
+  intros. apply finmap_eq. intros jj.
+  destruct (decide (jj = j)).
+  * subst. now rewrite lookup_partial_alter_ne,
+     !lookup_partial_alter, lookup_partial_alter_ne.
+  * destruct (decide (jj = i)).
+    + subst. now rewrite lookup_partial_alter,
+       !lookup_partial_alter_ne, lookup_partial_alter by congruence.
+    + now rewrite !lookup_partial_alter_ne by congruence.
+Qed.
+Lemma partial_alter_self_alt (m : M A) i x :
+  x = m !! i → partial_alter (λ _, x) i m = m.
+Proof.
+  intros. apply finmap_eq. intros ii.
+  destruct (decide (i = ii)).
+  * subst. now rewrite lookup_partial_alter.
+  * now rewrite lookup_partial_alter_ne.
+Qed.
+Lemma partial_alter_self (m : M A) i : partial_alter (λ _, m !! i) i m = m.
+Proof. now apply partial_alter_self_alt. Qed.
+
+Lemma lookup_insert (m : M A) i x : <[i:=x]>m !! i = Some x.
+Proof. unfold insert. apply lookup_partial_alter. Qed.
+Lemma lookup_insert_rev (m : M A) i x y : <[i:= x ]>m !! i = Some y → x = y.
+Proof. rewrite lookup_insert. congruence. Qed.
+Lemma lookup_insert_ne (m : M A) i j x : i ≠ j → <[i:=x]>m !! j = m !! j.
+Proof. unfold insert. apply lookup_partial_alter_ne. Qed.
+Lemma insert_comm (m : M A) i j x y :
+  i ≠ j → <[i:=x]>(<[j:=y]>m) = <[j:=y]>(<[i:=x]>m).
+Proof. apply partial_alter_comm. Qed.
+
+Lemma lookup_insert_Some (m : M A) i j x y :
+  <[i:=x]>m !! j = Some y ↔ (i = j ∧ x = y) ∨ (i ≠ j ∧ m !! j = Some y).
+Proof.
+  split.
+  * destruct (decide (i = j)); subst;
+      rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
+  * intros [[??]|[??]].
+    + subst. apply lookup_insert.
+    + now rewrite lookup_insert_ne.
+Qed.
+Lemma lookup_insert_None (m : M A) i j x :
+  <[i:=x]>m !! j = None ↔ m !! j = None ∧ i ≠ j.
+Proof.
+  split.
+  * destruct (decide (i = j)); subst;
+      rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
+  * intros [??]. now rewrite lookup_insert_ne.
+Qed.
+
+Lemma lookup_singleton_Some i j (x y : A) :
+  {[(i, x)]} !! j = Some y ↔ i = j ∧ x = y.
+Proof.
+  unfold singleton, finmap_singleton.
+  rewrite lookup_insert_Some, lookup_empty. simpl.
+  intuition congruence.
+Qed.
+Lemma lookup_singleton_None i j (x : A) :
+  {[(i, x)]} !! j = None ↔ i ≠ j.
+Proof.
+  unfold singleton, finmap_singleton.
+  rewrite lookup_insert_None, lookup_empty. simpl. tauto.
+Qed.
+
+Lemma lookup_singleton i (x : A) : {[(i, x)]} !! i = Some x.
+Proof. rewrite lookup_singleton_Some. tauto. Qed.
+Lemma lookup_singleton_ne i j (x : A) : i ≠ j → {[(i, x)]} !! j = None.
+Proof. now rewrite lookup_singleton_None. Qed.
+
+Lemma lookup_delete (m : M A) i : delete i m !! i = None.
+Proof. apply lookup_partial_alter. Qed.
+Lemma lookup_delete_ne (m : M A) i j : i ≠ j → delete i m !! j = m !! j.
+Proof. apply lookup_partial_alter_ne. Qed.
+
+Lemma lookup_delete_Some (m : M A) i j y :
+  delete i m !! j = Some y ↔ i ≠ j ∧ m !! j = Some y.
+Proof.
+  split.
+  * destruct (decide (i = j)); subst;
+      rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence.
+  * intros [??]. now rewrite lookup_delete_ne.
+Qed.
+Lemma lookup_delete_None (m : M A) i j :
+  delete i m !! j = None ↔ i = j ∨ m !! j = None.
+Proof.
+  destruct (decide (i = j)).
+  * subst. rewrite lookup_delete. tauto.
+  * rewrite lookup_delete_ne; tauto.
+Qed.
+
+Lemma delete_empty i : delete i (∅ : M A) = ∅.
+Proof. rewrite <-(partial_alter_self ∅) at 2. now rewrite lookup_empty. Qed.
+Lemma delete_singleton i (x : A) : delete i {[(i, x)]} = ∅.
+Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
+Lemma delete_comm (m : M A) i j : delete i (delete j m) = delete j (delete i m).
+Proof. destruct (decide (i = j)). now subst. now apply partial_alter_comm. Qed.
+Lemma delete_insert_comm (m : M A) i j x :
+  i ≠ j → delete i (<[j:=x]>m) = <[j:=x]>(delete i m).
+Proof. intro. now apply partial_alter_comm. Qed.
+
+Lemma delete_notin (m : M A) i : m !! i = None → delete i m = m.
+Proof.
+  intros. apply finmap_eq. intros j.
+  destruct (decide (i = j)).
+  * subst. now rewrite lookup_delete.
+  * now apply lookup_delete_ne.
+Qed.
+
+Lemma delete_partial_alter (m : M A) i f :
+  m !! i = None → delete i (partial_alter f i m) = m.
+Proof.
+  intros. unfold delete, finmap_delete. rewrite <-partial_alter_compose. 
+  rapply partial_alter_self_alt. congruence.
+Qed.
+Lemma delete_partial_alter_dom C `{Collection K C} (m : M A) i f : 
+  i ∉ dom C m → delete i (partial_alter f i m) = m.
+Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed.
+Lemma delete_insert (m : M A) i x : m !! i = None → delete i (<[i:=x]>m) = m.
+Proof. apply delete_partial_alter. Qed.
+Lemma delete_insert_dom C `{Collection K C} (m : M A) i x :
+  i ∉ dom C m → delete i (<[i:=x]>m) = m.
+Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed.
+Lemma insert_delete (m : M A) i x : m !! i = Some x → <[i:=x]>(delete i m) = m.
+Proof.
+  intros Hmi. unfold delete, finmap_delete, insert, finmap_insert.
+  rewrite <-partial_alter_compose. unfold compose. rewrite <-Hmi.
+  now apply partial_alter_self_alt.
+Qed.
+
+Lemma elem_of_dom_delete C `{Collection K C} (m : M A) i j :
+  i ∈ dom C (delete j m) ↔ i ≠ j ∧ i ∈ dom C m.
+Proof.
+  rewrite !(elem_of_dom C). unfold is_Some.
+  setoid_rewrite lookup_delete_Some. firstorder auto.
+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 partial_alter_compose (m : M A) i f g :
-    partial_alter (f ∘ g) i m = partial_alter f i (partial_alter g i m).
+Lemma lookup_delete_list (m : M A) is j :
+  In j is → delete_list is m !! j = None.
+Proof.
+  induction is as [|i is]; simpl; [easy |].
+  intros [?|?].
+  * subst. now rewrite lookup_delete.
+  * destruct (decide (i = j)).
+    + subst. now rewrite lookup_delete.
+    + rewrite lookup_delete_ne; auto.
+Qed.
+Lemma lookup_delete_list_notin (m : M A) is j :
+  ¬In j is → delete_list is m !! j = m !! j.
+Proof.
+  induction is; simpl; [easy |].
+  intros. rewrite lookup_delete_ne; tauto.
+Qed.
+
+Lemma delete_list_notin (m : M A) is :
+  Forall (λ i, m !! i = None) is → delete_list is m = m.
+Proof.
+  induction 1; simpl; [easy |].
+  rewrite delete_notin; congruence.
+Qed.
+Lemma delete_list_insert_comm (m : M A) is j x :
+  ¬In j is → delete_list is (<[j:=x]>m) = <[j:=x]>(delete_list is m).
+Proof.
+  induction is; simpl; [easy |].
+  intros. rewrite IHis, delete_insert_comm; tauto.
+Qed.
+
+Lemma finmap_ind C (P : M A → Prop) `{FinCollection K C} :
+  P ∅ → (∀ i x m, i ∉ dom C m → P m → P (<[i:=x]>m)) → ∀ m, P m.
+Proof.
+  intros Hemp Hinsert.
+  intros m. apply (collection_ind (λ X, ∀ m, dom C m ≡ X → P m)) with (dom C m).
+  * solve_proper.
+  * clear m. intros m Hm. rewrite finmap_empty.
+    + easy.
+    + intros. rewrite <-(not_elem_of_dom C), Hm.
+      now simplify_elem_of.
+  * clear m. intros i X Hi IH m Hdom.
+    assert (is_Some (m !! i)) as [x Hx].
+    { apply (elem_of_dom C).
+      rewrite Hdom. clear Hdom.
+      now simplify_elem_of. }
+    rewrite <-(insert_delete m i x) by easy.
+    apply Hinsert.
+    { now apply (not_elem_of_dom_delete C). }
+    apply IH. apply elem_of_equiv. intros.
+    rewrite (elem_of_dom_delete C). rewrite Hdom.
+    clear Hdom. simplify_elem_of.
+  * easy.
+Qed.
+
+Section merge.
+  Context (f : option A → option A → option A).
+
+  Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f).
   Proof.
-    intros. apply finmap_eq. intros ii. case (decide (i = ii)).
-     intros. subst. now rewrite !lookup_partial_alter.
-    intros. now rewrite !lookup_partial_alter_ne.
+    intros ??. apply finmap_eq. intros.
+    now rewrite !(merge_spec f), lookup_empty, (left_id None f).
   Qed.
-  Lemma partial_alter_comm (m : M A) i j f g :
-    i ≠ j → partial_alter f i (partial_alter g j m) = partial_alter g j (partial_alter f i m).
+  Global Instance: RightId (=) None f → RightId (=) ∅ (merge f).
   Proof.
-    intros. apply finmap_eq. intros jj. case (decide (jj = j)).
-     intros. subst. now rewrite lookup_partial_alter_ne, !lookup_partial_alter, lookup_partial_alter_ne.
-    intros. case (decide (jj = i)).
-     intros. subst. now rewrite lookup_partial_alter, !lookup_partial_alter_ne, lookup_partial_alter by congruence.
-    intros. now rewrite !lookup_partial_alter_ne by congruence.
+    intros ??. apply finmap_eq. intros.
+    now rewrite !(merge_spec f), lookup_empty, (right_id None f).
   Qed.
-  Lemma partial_alter_self_alt (m : M A) i x :
-    x = m !! i → partial_alter (λ _, x) i m = m.
+  Global Instance: Idempotent (=) f → Idempotent (=) (merge f).
+  Proof. intros ??. apply finmap_eq. intros. now 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.
-    intros. apply finmap_eq. intros ii. case (decide (i = ii)).
-     intros. subst. now rewrite lookup_partial_alter.
-    intros. now rewrite lookup_partial_alter_ne.
+    split; [| intro; subst; apply (merge_spec _) ].
+    intros Hlookup. apply finmap_eq. intros. rewrite Hlookup.
+    apply (merge_spec _).
   Qed.
-  Lemma partial_alter_self (m : M A) i : partial_alter (λ _, m !! i) i m = m.
-  Proof. now apply partial_alter_self_alt. Qed.
-
-  Lemma lookup_insert (m : M A) i x : <[ i := x ]> m !! i = Some x.
-  Proof. unfold insert. apply lookup_partial_alter. Qed.
-  Lemma lookup_insert_rev (m : M A) i x y : <[ i := x ]> m !! i = Some y → x = y.
-  Proof. rewrite lookup_insert. congruence. Qed.
-  Lemma lookup_insert_ne (m : M A) i j x : i ≠ j → <[ i := x ]> m !! j = m !! j.
-  Proof. unfold insert. apply lookup_partial_alter_ne. Qed.
-  Lemma insert_comm (m : M A) i j x y : i ≠ j → <[ i := x ]>(<[ j := y ]>m) = <[ j := y ]>(<[ i := x ]>m).
-  Proof. apply partial_alter_comm. Qed.
-
-  Lemma lookup_delete (m : M A) i : delete i m !! i = None.
-  Proof. apply lookup_partial_alter. Qed.
-  Lemma lookup_delete_Some (m : M A) i j : is_Some (delete i m !! j) → i ≠ j.
-  Proof. intros Hm ?. subst. rewrite lookup_delete in Hm. now apply None_not_is_Some in Hm. Qed.
-  Lemma lookup_delete_ne (m : M A) i j : i ≠ j → delete i m !! j = m !! j.
-  Proof. apply lookup_partial_alter_ne. Qed.
-  Lemma lookup_delete_None (m : M A) i j : m !! j = None → delete i m !! j = None.
+
+  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. now rewrite !(merge_spec f). Qed.
+  Global Instance: Commutative (=) f → Commutative (=) (merge f).
+  Proof. intros ???. apply merge_comm. intros. now 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. now rewrite !(merge_spec f). Qed.
+  Global Instance: Associative (=) f → Associative (=) (merge f).
+  Proof. intros ????. apply merge_assoc. intros. now apply (associative f). Qed.
+End merge.
+
+Section union_intersection.
+  Context (f : A → A → A).
+
+  Lemma finmap_union_merge m1 m2 i x y :
+    m1 !! i = Some x → m2 !! i = Some y → union_with f m1 m2 !! i = Some (f x y).
   Proof.
-    destruct (decide (i = j)).
-     subst. now rewrite lookup_delete.
-    now rewrite lookup_delete_ne.
-  Qed.
-  Lemma delete_lookup_None (m : M A) i : m !! i = None → delete i m = m.
+    intros Hx Hy. unfold union_with, finmap_union.
+    now rewrite (merge_spec _), Hx, Hy.
+  Qed.   
+  Lemma finmap_union_l m1 m2 i x :
+    m1 !! i = Some x → m2 !! i = None → union_with f m1 m2 !! i = Some x.
   Proof.
-    intros. apply finmap_eq. intros j. destruct (decide (i = j)).
-     subst. rewrite lookup_delete. congruence.
-    now apply lookup_delete_ne.
+    intros Hx Hy. unfold union_with, finmap_union.
+    now rewrite (merge_spec _), Hx, Hy.
   Qed.
-
-  Lemma delete_empty i : delete i (∅ : M A) = ∅.
-  Proof. rewrite <-(partial_alter_self ∅) at 2. now rewrite lookup_empty. Qed.
-  Lemma delete_singleton i (x : A) : delete i {{ (i, x) }} = ∅.
-  Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
-  Lemma delete_comm (m : M A) i j : delete i (delete j m) = delete j (delete i m).
-  Proof. destruct (decide (i = j)). now subst. now apply partial_alter_comm. Qed.
-  Lemma delete_partial_alter (m : M A) i f : m !! i = None → delete i (partial_alter f i m) = m.
+  Lemma finmap_union_r m1 m2 i y :
+    m1 !! i = None → m2 !! i = Some y → union_with f m1 m2 !! i = Some y.
   Proof.
-    intros. unfold delete, finmap_delete. rewrite <-partial_alter_compose. 
-    rapply partial_alter_self_alt. congruence.
+    intros Hx Hy. unfold union_with, finmap_union.
+    now rewrite (merge_spec _), Hx, Hy.
   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.
+  Lemma finmap_union_None m1 m2 i :
+    union_with f m1 m2 !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
   Proof.
-    intros Hmi. unfold delete, finmap_delete, insert, finmap_insert.
-    rewrite <-partial_alter_compose. unfold compose. rewrite <-Hmi.
-    now apply partial_alter_self_alt.
+    unfold union_with, finmap_union. rewrite (merge_spec _).
+    destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
   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). split.
-     intros. assert (j ≠ i) by (eapply lookup_delete_Some; eauto).
-     erewrite <-lookup_delete_ne; eauto.
-    intros [??]. now rewrite lookup_delete_ne by congruence.
-  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.
+  Global Instance: LeftId (=) ∅ (union_with f : M A → M A → M A) := _.
+  Global Instance: RightId (=) ∅ (union_with f : M A → M A → M A) := _.
+  Global Instance:
+    Commutative (=) f → Commutative (=) (union_with f : M A → M A → M A) := _.
+  Global Instance:
+    Associative (=) f → Associative (=) (union_with f : M A → M A → M A) := _.
+  Global Instance:
+    Idempotent (=) f → Idempotent (=) (union_with f : M A → M A → M A) := _.
+End union_intersection.
 
-  Lemma finmap_ind C (P : M A → Prop) `{FinCollection K C} :
-    P ∅ → (∀ i x m, i ∉ dom C m → P m → P (<[ i := x ]>m)) → ∀ m, P m.
-  Proof.
-    intros Hemp Hinsert.
-    intros m. apply (collection_ind (λ X, ∀ m, dom C m ≡ X → P m)) with (dom C m).
-       solve_proper.
-      clear m. intros m Hm. rewrite finmap_empty. easy.
-      intros. rewrite <-(not_elem_of_dom C), Hm. now simplify_elem_of.
-     clear m. intros i X Hi IH m Hdom.
-     assert (is_Some (m !! i)) as [x Hx].
-      apply (elem_of_dom C). rewrite Hdom. clear Hdom. now simplify_elem_of.
-     rewrite <-(insert_delete m i x) by easy. apply Hinsert.
-      now apply (not_elem_of_dom_delete C).
-     apply IH. apply elem_of_equiv. intros.
-     rewrite (elem_of_dom_delete C). rewrite Hdom.
-     clear Hdom. simplify_elem_of.
-    easy.
-  Qed.
+Lemma lookup_insert_list (m : M A) l1 l2 i x :
+  (∀y, ¬In (i,y) l1) → insert_list (l1 ++ (i,x) :: l2) m !! i = Some x.
+Proof.
+  induction l1 as [|[j y] l1 IH]; simpl.
+   intros. now rewrite lookup_insert.
+  intros Hy. rewrite lookup_insert_ne. apply IH.
+   firstorder.
+  intro. apply (Hy y). left. congruence.
+Qed.
 
-  Section merge.
-    Context (f : option A → option A → option A).
-
-    Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f).
-    Proof.
-      intros ??. apply finmap_eq. intros.
-      now 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.
-      now rewrite !(merge_spec f), lookup_empty, (right_id None f).
-    Qed.
-    Global Instance: Idempotent (=) f → Idempotent (=) (merge f).
-    Proof. intros ??. apply finmap_eq. intros. now 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. now rewrite !(merge_spec f). Qed.
-    Global Instance: Commutative (=) f → Commutative (=) (merge f).
-    Proof. intros ???. apply merge_comm. intros. now 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. now rewrite !(merge_spec f). Qed.
-    Global Instance: Associative (=) f → Associative (=) (merge f).
-    Proof. intros ????. apply merge_assoc. intros. now apply (associative f). Qed.
-  End merge.
-
-  Section union_intersect.
-    Context (f : A → A → A).
-
-    Lemma finmap_union_merge m1 m2 i x y :
-      m1 !! i = Some x → m2 !! i = Some y → union_with f m1 m2 !! i = Some (f x y).
-    Proof. intros Hx Hy. unfold union_with, finmap_union. now rewrite (merge_spec _), Hx, Hy. Qed.   
-    Lemma finmap_union_l m1 m2 i x :
-      m1 !! i = Some x → m2 !! i = None → union_with f m1 m2 !! i = Some x.
-    Proof. intros Hx Hy. unfold union_with, finmap_union. now rewrite (merge_spec _), Hx, Hy. Qed.
-    Lemma finmap_union_r m1 m2 i y :
-      m1 !! i = None → m2 !! i = Some y → union_with f m1 m2 !! i = Some y.
-    Proof. intros Hx Hy. unfold union_with, finmap_union. now rewrite (merge_spec _), Hx, Hy. Qed.
-    Lemma finmap_union_None m1 m2 i :
-      union_with f m1 m2 !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
-    Proof.
-      unfold union_with, finmap_union. rewrite (merge_spec _).
-      destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
-    Qed.
-
-    Global Instance: LeftId (=) ∅ (union_with f : M A → M A → M A) := _.
-    Global Instance: RightId (=) ∅ (union_with f : M A → M A → M A) := _.
-    Global Instance: Commutative (=) f → Commutative (=) (union_with f : M A → M A → M A) := _.
-    Global Instance: Associative (=) f → Associative (=) (union_with f : M A → M A → M A) := _.
-    Global Instance: Idempotent (=) f → Idempotent (=) (union_with f : M A → M A → M A) := _.
-  End union_intersect.
+Lemma lookup_insert_list_not_in (m : M A) l i :
+  (∀y, ¬In (i,y) l) → insert_list l m !! i = m !! i.
+Proof.
+  induction l as [|[j y] l IH]; simpl.
+   easy.
+  intros Hy. rewrite lookup_insert_ne.
+   firstorder.
+  intro. apply (Hy y). left. congruence.
+Qed.
 End finmap.
+
+Tactic Notation "simplify_map" "by" tactic(T) := repeat
+  match goal with
+  | _ => progress simplify_eqs
+  | H : context[ ∅ !! _ ] |- _ => rewrite lookup_empty in H
+  | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert in H
+  | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert_ne in H by T
+  | H : context[ (delete _ _) !! _ ] |- _ => rewrite lookup_delete in H
+  | H : context[ (delete _ _) !! _ ] |- _ => rewrite lookup_delete_ne in H by T
+  | H : context[ {[ _ ]} !! _ ] |- _ => rewrite lookup_singleton in H
+  | H : context[ {[ _ ]} !! _ ] |- _ => rewrite lookup_singleton_ne in H by T
+  | |- context[ ∅ !! _ ] => rewrite lookup_empty
+  | |- context[ (<[_:=_]>_) !! _ ] => rewrite lookup_insert
+  | |- context[ (<[_:=_]>_) !! _ ] => rewrite lookup_insert_ne by T
+  | |- context[ (delete _ _) !! _ ] => rewrite lookup_delete
+  | |- context[ (delete _ _) !! _ ] => rewrite lookup_delete_ne by T
+  | |- context[ {[ _ ]} !! _ ] => rewrite lookup_singleton
+  | |- context[ {[ _ ]} !! _ ] => rewrite lookup_singleton_ne by T
+  end.
+Tactic Notation "simplify_map" := simplify_map by auto.
diff --git a/theories/list.v b/theories/list.v
index ef554c83..975e2078 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -15,18 +15,118 @@ Notation "(++)" := app (only parsing) : C_scope.
 Notation "( l ++)" := (app l) (only parsing) : C_scope.
 Notation "(++ k )" := (λ l, app l k) (only parsing) : C_scope.
 
+Global Instance list_lookup: Lookup nat list :=
+  fix list_lookup A (i : nat) (l : list A) {struct l} : option A :=
+  match l with
+  | [] => None
+  | x :: l =>
+    match i with
+    | 0 => Some x
+    | S i => @lookup _ _ list_lookup _ i l
+    end
+  end.
+
+(* The [simpl] tactic does not unfold [list_lookup] as it is wrapped into
+a type class. Therefore we use the following tactic. Bug: does not simplify
+under binders.
+*)
+Ltac simplify_list_lookup := repeat
+  match goal with
+  | |- context f [@nil ?A !! _] => let X := (context f [@None A]) in change X
+  | |- context f [(?x :: _) !! 0] => let X := (context f [Some x]) in change X
+  | |- context f [(_ :: ?l) !! S ?i] => let X := (context f [l !! i]) in change X
+  | H : context f [@nil ?A !! _] |- _ => let X := (context f [@None A]) in change X in H
+  | H : context f [(?x :: _) !! 0] |- _ => let X := (context f [Some x]) in change X in H
+  | H : context f [(_ :: ?l) !! S ?i] |- _  => let X := (context f [l !! i]) in change X in H
+  end.
+
+Global Instance list_alter: Alter nat list :=
+  fix list_alter A (f : A → A) (i : nat) (l : list A) {struct l} :=
+  match l with
+  | [] => []
+  | x :: l =>
+    match i with
+    | 0 => f x :: l
+    | S i => x :: @alter _ _ list_alter _ f i l
+    end
+  end.
+
+Definition option_list {A} : option A → list A := option_rect _ (λ x, [x]) [].
+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.
+
 Section list_properties.
 Context {A : Type}.
 
-Definition option_list : option A → list A := option_rect _ (λ x, [x]) [].
+Lemma list_eq (l1 l2 : list A) : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
+Proof.
+  revert l2. induction l1; intros [|??] H.
+  * easy.
+  * discriminate (H 0).
+  * discriminate (H 0).
+  * f_equal. now injection (H 0). apply IHl1. intro. apply (H (S _)).
+Qed.
+
+Lemma list_lookup_nil i : @nil A !! i = None.
+Proof. now destruct i. Qed.
+Lemma list_lookup_tail (l : list A) i : tail l !! i = l !! S i.
+Proof. now destruct l. Qed.
+
+Lemma list_lookup_Some_In (l : list A) i x : l !! i = Some x → In x l.
+Proof.
+  revert i. induction l; intros [|i] ?;
+    simplify_list_lookup; simplify_eqs; constructor (solve [eauto]).
+Qed.
+
+Lemma list_lookup_In_Some (l : list A) x : In x l → ∃ i, l !! i = Some x.
+Proof.
+  induction l; destruct 1; subst.
+  * now exists 0.
+  * destruct IHl as [i ?]; auto. now exists (S i).
+Qed.
+Lemma list_lookup_In (l : list A) x : In x l ↔ ∃ i, l !! i = Some x.
+Proof. firstorder eauto using list_lookup_Some_In, list_lookup_In_Some. Qed.
+
+Lemma list_lookup_app_length (l1 l2 : list A) (x : A) :
+  (l1 ++ x :: l2) !! length l1 = Some x.
+Proof. induction l1; simpl; now simplify_list_lookup. Qed.
+
+Lemma list_lookup_lt_length (l : list A) i : is_Some (l !! i) ↔ i < length l.
+Proof.
+  revert i. induction l.
+  * split; now inversion 1.
+  * intros [|?]; simplify_list_lookup; simpl.
+    + split; auto with arith.
+    + now rewrite <-NPeano.Nat.succ_lt_mono.
+Qed.
+Lemma list_lookup_weaken (l l' : list A) i x :
+  l !! i = Some x → (l ++ l') !! i = Some x.
+Proof. revert i. induction l. discriminate. now intros []. Qed.
+
+Lemma Forall_impl (P Q : A → Prop) l :
+  Forall P l → (∀ x, P x → Q x) → Forall Q l.
+Proof. induction 1; auto. Qed.
+
+Lemma Forall2_length {B} (P : A → B → Prop) l1 l2 :
+  Forall2 P l1 l2 → length l1 = length l2.
+Proof. induction 1; simpl; auto. Qed.
+
+Lemma Forall2_impl {B} (P Q : A → B → Prop) l1 l2 :
+  Forall2 P l1 l2 → (∀ x y, P x y → Q x y) → Forall2 Q l1 l2.
+Proof. induction 1; auto. Qed.
+
+Lemma Forall2_unique {B} (P : A → B → Prop) l k1 k2 :
+  Forall2 P l k1 → Forall2 P l k2 → (∀ x y1 y2, P x y1 → P x y2 → y1 = y2) → k1 = k2.
+Proof. intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto. Qed.
 
 Lemma NoDup_singleton (x : A) : NoDup [x].
 Proof. constructor. easy. constructor. Qed.
 Lemma NoDup_app (l k : list A) :
   NoDup l → NoDup k → (∀ x, In x l → ¬In x k) → NoDup (l ++ k).
 Proof.
-  induction 1; simpl. easy.
-  constructor. rewrite in_app_iff. firstorder. firstorder.
+  induction 1; simpl.
+  * easy.
+  * constructor. rewrite in_app_iff. firstorder. firstorder.
 Qed.
 
 Global Instance: ∀ k : list A, Injective (=) (=) (k ++).
@@ -47,12 +147,13 @@ Proof. now inversion 1. Qed.
 Lemma Exists_inv (P : A → Prop) x l : Exists P (x :: l) → P x ∨ Exists P l.
 Proof. inversion 1; intuition. Qed.
 
-Global Instance list_eq_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ l k : list A, Decision (l = k).
-Proof. solve_decision. Qed.
+Global Instance list_eq_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ l k,
+  Decision (l = k) := list_eq_dec dec.
 Global Instance list_in_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ x l,
   Decision (In x l) := in_dec dec.
 
-Global Instance NoDup_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ (l : list A), Decision (NoDup l) :=
+Global Instance NoDup_dec {dec : ∀ x y : A, Decision (x = y)} :
+    ∀ (l : list A), Decision (NoDup l) :=
   fix NoDup_dec l :=
   match l return Decision (NoDup l) with
   | [] => left NoDup_nil
@@ -67,7 +168,8 @@ Global Instance NoDup_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ (l : list
     end
   end.
 
-Global Instance Forall_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} : ∀ l, Decision (Forall P l) :=
+Global Instance Forall_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} :
+    ∀ l, Decision (Forall P l) :=
   fix go (l : list A) :=
   match l return {Forall P l} + {¬Forall P l} with
   | [] => left (Forall_nil _)
@@ -82,7 +184,8 @@ Global Instance Forall_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} : ∀
     end
   end.
 
-Global Instance Exists_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} : ∀ l, Decision (Exists P l) :=
+Global Instance Exists_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} :
+    ∀ l, Decision (Exists P l) :=
   fix go (l : list A) :=
   match l return {Exists P l} + {¬Exists P l} with
   | [] => right (proj1 (Exists_nil _))
@@ -97,33 +200,36 @@ Global Instance Exists_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} : ∀
     end
   end.
 
-Definition prefix_of (l1 l2 : list A) : Prop := ∃ k, l2 = l1 ++ k.
-Definition suffix_of (l1 l2 : list A) : Prop := ∃ k, l2 = k ++ l1.
-
-Global Instance: PreOrder prefix_of.
+Global Instance: PreOrder (@prefix_of A).
 Proof.
   split.
    intros ?. eexists []. now rewrite app_nil_r.
   intros ??? [k1 ?] [k2 ?]. exists (k1 ++ k2). subst. now rewrite app_assoc.
 Qed.
 
-Lemma prefix_of_nil l : prefix_of [] l.
+Lemma prefix_of_nil (l : list A) : prefix_of [] l.
 Proof. now exists l. Qed.
-Lemma prefix_of_nil_not x l : ¬prefix_of (x :: l) [].
+Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) [].
 Proof. intros [k E]. discriminate. Qed.
-Lemma prefix_of_cons x y l1 l2 : x = y → prefix_of l1 l2 → prefix_of (x :: l1) (y :: l2).
+Lemma prefix_of_cons x y (l1 l2 : list A) :
+  x = y → prefix_of l1 l2 → prefix_of (x :: l1) (y :: l2).
 Proof. intros ? [k E]. exists k. now subst. Qed.
-Lemma prefix_of_cons_inv_1 x y l1 l2 : prefix_of (x :: l1) (y :: l2) → x = y.
+Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) :
+  prefix_of (x :: l1) (y :: l2) → x = y.
 Proof. intros [k E]. now injection E. Qed.
-Lemma prefix_of_cons_inv_2 x y l1 l2 : prefix_of (x :: l1) (y :: l2) → prefix_of l1 l2.
+Lemma prefix_of_cons_inv_2 x y (l1 l2 : list A) :
+  prefix_of (x :: l1) (y :: l2) → prefix_of l1 l2.
 Proof. intros [k E]. exists k. now injection E. Qed.
 
-Lemma prefix_of_app_l l1 l2 l3 : prefix_of (l1 ++ l3) l2 → prefix_of l1 l2.
+Lemma prefix_of_app_l (l1 l2 l3 : list A) :
+  prefix_of (l1 ++ l3) l2 → prefix_of l1 l2.
 Proof. intros [k ?]. red. exists (l3 ++ k). subst. now rewrite <-app_assoc. Qed.
-Lemma prefix_of_app_r l1 l2 l3 : prefix_of l1 l2 → prefix_of l1 (l2 ++ l3).
+Lemma prefix_of_app_r (l1 l2 l3 : list A) :
+  prefix_of l1 l2 → prefix_of l1 (l2 ++ l3).
 Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite app_assoc. Qed.
 
-Global Instance prefix_of_dec `{∀ x y : A, Decision (x = y)} : ∀ l1 l2, Decision (prefix_of l1 l2) :=
+Global Instance prefix_of_dec `{∀ x y : A, Decision (x = y)} :
+    ∀ l1 l2, Decision (prefix_of l1 l2) :=
   fix prefix_of_dec l1 l2 :=
   match l1, l2 return { prefix_of l1 l2 } + { ¬prefix_of l1 l2 } with
   | [], _ => left (prefix_of_nil _)
@@ -139,63 +245,77 @@ Global Instance prefix_of_dec `{∀ x y : A, Decision (x = y)} : ∀ l1 l2, Deci
     end
   end.
 
-Global Instance: PreOrder suffix_of.
+Global Instance: PreOrder (@suffix_of A).
 Proof.
   split.
-   intros ?. now eexists [].
-  intros ??? [k1 ?] [k2 ?]. exists (k2 ++ k1). subst. now rewrite app_assoc.
+  * intros ?. now eexists [].
+  * intros ??? [k1 ?] [k2 ?].
+    exists (k2 ++ k1). subst. now rewrite app_assoc.
 Qed.
 
-Lemma prefix_suffix_rev l1 l2 : prefix_of l1 l2 ↔ suffix_of (rev l1) (rev l2).
+Lemma prefix_suffix_rev (l1 l2 : list A) :
+  prefix_of l1 l2 ↔ suffix_of (rev l1) (rev l2).
 Proof.
   split; intros [k E]; exists (rev k).
-   now rewrite E, rev_app_distr.
-  now rewrite <-(rev_involutive l2), E, rev_app_distr, rev_involutive.
+  * now rewrite E, rev_app_distr.
+  * now rewrite <-(rev_involutive l2), E, rev_app_distr, rev_involutive.
 Qed.
-Lemma suffix_prefix_rev l1 l2 : suffix_of l1 l2 ↔ prefix_of (rev l1) (rev l2).
+Lemma suffix_prefix_rev (l1 l2 : list A) :
+  suffix_of l1 l2 ↔ prefix_of (rev l1) (rev l2).
 Proof. now rewrite prefix_suffix_rev, !rev_involutive. Qed.
 
-Lemma suffix_of_nil l : suffix_of [] l.
+Lemma suffix_of_nil (l : list A) : suffix_of [] l.
 Proof. exists l. now rewrite app_nil_r. Qed.
-Lemma suffix_of_nil_not x l : ¬suffix_of (x :: l) [].
+Lemma suffix_of_nil_not x (l : list A) : ¬suffix_of (x :: l) [].
 Proof. intros [[] ?]; discriminate. Qed.
-Lemma suffix_of_cons x y l1 l2 : x = y → suffix_of l1 l2 → suffix_of (l1 ++ [x]) (l2 ++ [y]).
+Lemma suffix_of_cons x y (l1 l2 : list A) :
+  x = y → suffix_of l1 l2 → suffix_of (l1 ++ [x]) (l2 ++ [y]).
 Proof. intros ? [k E]. exists k. subst. now rewrite app_assoc. Qed.
-Lemma suffix_of_snoc_inv_1 x y l1 l2 : suffix_of (l1 ++ [x]) (l2 ++ [y]) → x = y.
+Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) :
+  suffix_of (l1 ++ [x]) (l2 ++ [y]) → x = y.
 Proof. rewrite suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_1. Qed.
-Lemma suffix_of_snoc_inv_2 x y l1 l2 : suffix_of (l1 ++ [x]) (l2 ++ [y]) → suffix_of l1 l2.
+Lemma suffix_of_snoc_inv_2 x y (l1 l2 : list A) :
+  suffix_of (l1 ++ [x]) (l2 ++ [y]) → suffix_of l1 l2.
 Proof. rewrite !suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_2. Qed.
 
-Lemma suffix_of_cons_l l1 l2 x : suffix_of (x :: l1) l2 → suffix_of l1 l2.
+Lemma suffix_of_cons_l (l1 l2 : list A) x :
+  suffix_of (x :: l1) l2 → suffix_of l1 l2.
 Proof. intros [k ?]. exists (k ++ [x]). subst. now rewrite <-app_assoc. Qed.
-Lemma suffix_of_app_l l1 l2 l3 : suffix_of (l3 ++ l1) l2 → suffix_of l1 l2.
+Lemma suffix_of_app_l (l1 l2 l3 : list A) :
+  suffix_of (l3 ++ l1) l2 → suffix_of l1 l2.
 Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite <-app_assoc. Qed.
-Lemma suffix_of_cons_r l1 l2 x : suffix_of l1 l2 → suffix_of l1 (x :: l2).
+Lemma suffix_of_cons_r (l1 l2 : list A) x :
+  suffix_of l1 l2 → suffix_of l1 (x :: l2).
 Proof. intros [k ?]. exists (x :: k). now subst. Qed.
-Lemma suffix_of_app_r l1 l2 l3 : suffix_of l1 l2 → suffix_of l1 (l3 ++ l2).
+Lemma suffix_of_app_r (l1 l2 l3 : list A) :
+  suffix_of l1 l2 → suffix_of l1 (l3 ++ l2).
 Proof. intros [k ?]. exists (l3 ++ k). subst. now rewrite app_assoc. Qed.
 
-Lemma suffix_of_cons_inv l1 l2 x y : 
+Lemma suffix_of_cons_inv (l1 l2 : list A) x y : 
   suffix_of (x :: l1) (y :: l2) → x :: l1 = y :: l2 ∨ suffix_of (x :: l1) l2.
 Proof.
   intros [[|? k] E].
    now left.
   right. simplify_eqs. now apply suffix_of_app_r.
 Qed.
-Lemma suffix_of_cons_not x l : ¬suffix_of (x :: l) l.
+Lemma suffix_of_cons_not x (l : list A) : ¬suffix_of (x :: l) l.
 Proof.
   intros [k E]. change ([] ++ l = k ++ [x] ++ l) in E.
   rewrite app_assoc in E. apply app_inv_tail in E.
   destruct k; simplify_eqs.
 Qed.
 
-Global Program Instance suffix_of_dec `{∀ x y : A, Decision (x = y)} l1 l2 : Decision (suffix_of l1 l2) :=
+Global Program Instance suffix_of_dec `{∀ x y : A, Decision (x = y)} l1 l2 :
+    Decision (suffix_of l1 l2) :=
   match decide_rel prefix_of (rev_append l1 []) (rev_append l2 []) with
   | left Hpre => left _
   | right Hpre => right _
   end.
 Next Obligation. apply suffix_prefix_rev. now rewrite !rev_alt. Qed.
-Next Obligation. intro. destruct Hpre. rewrite <-!rev_alt. now apply suffix_prefix_rev. Qed.
+Next Obligation. 
+  intro. destruct Hpre. rewrite <-!rev_alt. 
+  now apply suffix_prefix_rev.
+Qed.
 End list_properties.
 
 Hint Resolve suffix_of_nil suffix_of_cons_r suffix_of_app_r : list.
@@ -205,49 +325,27 @@ Hint Extern 0 (PropHolds (suffix_of _ _)) => red; auto with list : typeclass_ins
 
 Ltac simplify_suffix_of := repeat
   match goal with
-  | H : suffix_of (_ :: _) _ |- _ => destruct (suffix_of_cons_not _ _ H); clear H
-  | H : suffix_of (_ :: _) [] |- _ => destruct (suffix_of_nil_not _ _ H); clear H
-  | H : suffix_of (_ :: _) (_ :: _) |- _ => destruct (suffix_of_cons_inv _ _ _ _ H); clear H
+  | H : suffix_of (_ :: _) _ |- _ => destruct (suffix_of_cons_not _ _ H)
+  | H : suffix_of (_ :: _) [] |- _ => destruct (suffix_of_nil_not _ _ H)
+  | H : suffix_of (_ :: _) (_ :: _) |- _ =>
+    destruct (suffix_of_cons_inv _ _ _ _ H); clear H
   | H : suffix_of ?x ?x |- _ => clear H
   | H : suffix_of ?x (_ :: ?x) |- _ => clear H
   | H : suffix_of ?x (_ ++ ?x) |- _ => clear H
   | _ => progress simplify_eqs
   end.
 
-Global Instance list_lookup: Lookup nat list :=
-  fix list_lookup A (i : nat) (l : list A) {struct l} : option A :=
-  match l with
-  | [] => None
-  | x :: l =>
-    match i with
-    | 0 => Some x
-    | S i => @lookup _ _ list_lookup _ i l
-    end
-  end.
-Local Arguments lookup _ _ _ _ _ !_ /.
-
-Global Instance list_alter: Alter nat list :=
-  fix list_alter A (f : A → A) (i : nat) (l : list A) {struct l} :=
-  match l with
-  | [] => []
-  | x :: l =>
-    match i with
-    | 0 => f x :: l
-    | S i => x :: @alter _ _ list_alter _ f i l
-    end
-  end.
-
-Lemma list_eq {A} (l1 l2 : list A) : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
-Proof.
-  revert l2. induction l1; intros [|??] H.
-     easy.
-    discriminate (H 0).
-   discriminate (H 0).
-  f_equal. now injection (H 0). apply IHl1. intro. apply (H (S _)).
-Qed.
-
-Lemma list_lookup_tail {A} (l : list A) i : tail l !! i = l !! S i.
-Proof. now destruct l. Qed.
+(* Extremely dirty way to discrimate inconsistent suffix_of assumptions *)
+Ltac discriminate_suffix_of := solve [repeat
+  match goal with
+  | _ => progress simplify_suffix_of
+  | H1 : suffix_of ?x ?y, H2 : suffix_of ?y ?z |- _ =>
+     match goal with
+     | _ : suffix_of x z |- _ => fail 2
+     | _ => assert (suffix_of x z) by (transitivity y; assumption);
+                 clear H1; clear H2 (* to avoid loops *)
+     end
+  end].
 
 Global Instance list_ret: MRet list := λ A a, [a].
 Global Instance list_fmap: FMap list :=
@@ -264,78 +362,122 @@ Global Instance list_join: MJoin list :=
   end.
 Global Instance list_bind: MBind list := λ A B f l, mjoin (f <$> l).
 
-Lemma list_lookup_weaken {A} (l l' : list A) i x :
-  l !! i = Some x → (l ++ l') !! i = Some x.
-Proof. revert i. induction l. discriminate. now intros []. Qed.
+Local Arguments fmap _ _ _ _ _ !_ /.
 
-Lemma list_lookup_fmap {A B} (f : A → B) l i : (f <$> l) !! i = f <$> (l !! i).
-Proof. revert i. induction l; now intros [|]. Qed.
+Section list_fmap.
+  Context {A B : Type} (f : A → B).
 
-Lemma fold_right_permutation `(f : A → B → B) (b : B) :
-  (∀ a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) → Proper (Permutation ==> (=)) (fold_right f b).
-Proof. intros Hflip. induction 1; simpl; try congruence. Qed.
-
-(*
-Section NoDupA.
-  Fixpoint removeDups (l : list A) : list A :=
-    match l with
-    | [] => []
-    | x :: l =>
-      let k := removeDups l in
-      if InA_dec dec x k then k else x :: k
-    end.
-
-  Lemma removeDups_NoDupA l : NoDupA R (removeDups l).
-  Proof. induction l; simpl; try case InA_dec; intuition. Qed.
-
-  Definition elem_removeDups x l : x ∈ removeDups l → x ∈ l.
+  Lemma fmap_length l : length (f <$> l) = length l.
+  Proof. induction l; simpl; auto. Qed.
+
+  Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
+  Proof. revert i. induction l; now intros [|]. Qed.
+
+  Lemma in_fmap_1 l x : In x l → In (f x) (f <$> l).
+  Proof. induction l; destruct 1; subst; constructor (solve [auto]). Qed.
+  Lemma in_fmap_1_alt l x y : In x l → y = f x → In y (f <$> l).
+  Proof. intros. subst. now apply in_fmap_1. Qed.
+  Lemma in_fmap_2 l x : In x (f <$> l) → ∃ y, x = f y ∧ In y l.
+  Proof.
+    induction l as [|y l]; destruct 1; subst.
+    * exists y; now intuition.
+    * destruct IHl as [y' [??]]. easy. exists y'; now intuition.
+  Qed.
+  Lemma in_fmap l x : In x (f <$> l) ↔ ∃ y, x = f y ∧ In y l.
   Proof.
-    induction l; simpl; auto.
-    case InA_dec; eauto.
-    intros ? Hin. destruct (list_elem_inv _ _ _ Hin); subst; eauto.
+    split.
+    * apply in_fmap_2.
+    * intros [? [??]]. eauto using in_fmap_1_alt.
   Qed.
+End list_fmap.
+
+Lemma Forall_fst {A B} (l : list (A * B)) (P : A → Prop) :
+  Forall (P ∘ fst) l ↔ Forall P (fst <$> l).
+Proof. induction l; split; inversion 1; subst; constructor; firstorder auto. Qed.
+Lemma Forall_snd {A B} (l : list (A * B)) (P : B → Prop) :
+  Forall (P ∘ snd) l ↔ Forall P (snd <$> l).
+Proof. induction l; split; inversion 1; subst; constructor; firstorder auto. Qed.
+
+Definition imap_go {A B} (f : nat → A → B) : nat → list A → list B :=
+  fix go (n : nat) (l : list A) :=
+  match l with
+  | [] => []
+  | x :: l => f n x :: go (S n) l
+  end.
+Definition imap {A B} (f : nat → A → B) : list A → list B := imap_go f 0.
 
-  Lemma elem_InA x y l : x ∈ l → R y x → InA R y l.
-  Proof. induction 1; subst; intuition. Qed.
+Lemma fold_right_permutation `(f : A → B → B) (b : B) :
+  (∀ a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) →
+  Proper (Permutation ==> (=)) (fold_right f b).
+Proof. intro. induction 1; simpl; congruence. Qed.
+
+Definition ifold_right {A B} (f : nat → B → A → A) (a : nat → A) : nat → list B → A :=
+  fix go (n : nat) (l : list B) : A :=
+  match l with
+  | nil => a n
+  | b :: l => f n b (go (S n) l)
+  end.
 
-  Lemma InA_elem x l : InA R x l → ∃ y, y ∈ l ∧ R x y.
-  Proof. induction 1. eauto. destruct IHInA as [? [??]]; eauto. Qed.
+Lemma ifold_right_app {A B} (f : nat → B → A → A) (a : nat → A) (l1 l2 : list B) n :
+  ifold_right f a n (l1 ++ l2) = ifold_right f (λ n, ifold_right f a n l2) n l1.
+Proof. revert n a. induction l1 as [| b l1 IH ]; intros; simpl; f_equal; auto. Qed.
 
-  Context `{!Equivalence R}.
+Section same_length.
+  Context {A B : Type}.
 
-  Lemma in_removeDups_inv x l : x ∈ l → ∃ y, y ∈ l ∧ R x y ∧ y ∈ removeDups l.
+  Inductive same_length : list A → list B → Prop :=
+    | same_length_nil : 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.
   Proof.
-    induction l as [|y l]; simpl.
-     inversion 1.
-    case InA_dec.
-     inversion 2; subst.
-      destruct (InA_elem y (removeDups l)) as [z [??]]; auto.
-      exists z. intuition. right. now apply elem_removeDups.
-     destruct IHl as [z [?[??]]]. auto. exists z. intuition.
-    intros ? Hin. destruct (list_elem_inv _ _ _ Hin).
-     subst. exists y. intuition.
-    destruct IHl as [z [?[??]]]. easy. exists z. intuition.
+    split.
+    * induction 1; simpl; auto.
+    * revert k. induction l; intros [|??]; try discriminate;
+      constructor; auto with arith.
   Qed.
 
-  Lemma in_removeDups x l : InA R x l ↔ InA R x (removeDups l).
+  Lemma same_length_lookup l k i :
+    same_length l k → is_Some (l !! i) → is_Some (k !! i).
   Proof.
-    split.
-     induction 1 as [?? E|]; simpl; [rewrite E|]; case InA_dec; intuition.
-    induction l; simpl; auto.
-    case InA_dec. auto. inversion_clear 2; auto.
+    rewrite same_length_length.
+    setoid_rewrite list_lookup_lt_length.
+    intros E. now rewrite E.
   Qed.
-End NoDupA.
+End same_length.
 
-Lemma InA_lift_rel {A B} (R : relation A) (f : B → A) x l : InA R (f x) (f <$> l) ↔ InA (lift_rel R f) x l.
-Proof. split; induction l; unfold fmap; simpl; inversion_clear 1; auto. Qed.
+Notation zip := combine.
 
-Lemma NoDupA_lift_rel {A B} (R : relation A) (f : B → A) l : NoDupA R (f <$> l) ↔ NoDupA (lift_rel R f) l.
-Proof.
-  split.
-   induction l; [easy |].
-   intros HnoDup. constructor.
-    intro. destruct (NoDupA_inv_1 R _ _ HnoDup). now apply InA_lift_rel.
-   eapply IHl, NoDupA_inv_2; eauto.
-  induction 1; constructor. now rewrite InA_lift_rel. easy.
-Qed.
-*)
+Section zip.
+  Context {A B : Type}.
+
+  Lemma zip_fst_le (l1 : list A) (l2 : list B) :
+    length l1 ≤ length l2 → fst <$> zip l1 l2 = l1.
+  Proof.
+    revert l2.
+    induction l1; intros [|??] ?; simpl; f_equal; auto with arith.
+    edestruct Le.le_Sn_0; eauto.
+  Qed.
+  Lemma zip_fst (l1 : list A) (l2 : list B) :
+    same_length l1 l2 → fst <$> zip l1 l2 = l1.
+  Proof.
+    rewrite same_length_length. intros H.
+    apply zip_fst_le. now rewrite H.
+  Qed.
+
+  Lemma zip_snd_le (l1 : list A) (l2 : list B) :
+    length l2 ≤ length l1 → snd <$> zip l1 l2 = l2.
+  Proof.
+    revert l2.
+    induction l1; intros [|??] ?; simpl; f_equal; auto with arith.
+    edestruct Le.le_Sn_0; eauto.
+  Qed.
+  Lemma zip_snd (l1 : list A) (l2 : list B) :
+    same_length l1 l2 → snd <$> zip l1 l2 = l2.
+  Proof.
+    rewrite same_length_length. intros H.
+    apply zip_snd_le. now rewrite H.
+  Qed.
+End zip.
diff --git a/theories/listset.v b/theories/listset.v
index 4006ad24..2af31ad9 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -7,59 +7,71 @@ Context {A : Type} `{∀ x y : A, Decision (x = y)}.
 
 Global Instance listset_elem_of: ElemOf A (listset A) := λ x l, In x (`l).
 Global Instance listset_empty: Empty (listset A) := []↾@NoDup_nil _.
-Global Instance listset_singleton: Singleton A (listset A) := λ x, [x]↾NoDup_singleton x.
+Global Instance listset_singleton: Singleton A (listset A) := λ x,
+  [x]↾NoDup_singleton x.
 
-Fixpoint listset_diff_raw (l k : list A) :=
+Fixpoint listset_difference_raw (l k : list A) :=
   match l with
   | [] => []
-  | x :: l => if decide_rel In x k then listset_diff_raw l k else x :: listset_diff_raw l k
+  | x :: l =>
+    if decide_rel In x k
+    then listset_difference_raw l k
+    else x :: listset_difference_raw l k
   end.
-Lemma listset_diff_raw_in l k x : In x (listset_diff_raw l k) ↔ In x l ∧ ¬In x k.
+Lemma listset_difference_raw_in l k x : In x (listset_difference_raw l k) ↔ In x l ∧ ¬In x k.
 Proof. split; induction l; simpl; try case_decide; simpl; intuition congruence. Qed.
-Lemma listset_diff_raw_nodup l k : NoDup l → NoDup (listset_diff_raw l k).
+Lemma listset_difference_raw_nodup l k : NoDup l → NoDup (listset_difference_raw l k).
 Proof. 
   induction 1; simpl; try case_decide.
-    constructor.
-   easy.
-  constructor. rewrite listset_diff_raw_in; intuition. easy.
+  * constructor.
+  * easy.
+  * constructor. rewrite listset_difference_raw_in; intuition. easy.
 Qed.
-Global Instance listset_diff: Difference (listset A) := λ l k,
-  listset_diff_raw (`l) (`k)↾listset_diff_raw_nodup (`l) (`k) (proj2_sig l).
+Global Instance listset_difference: Difference (listset A) := λ l k,
+  listset_difference_raw (`l) (`k)↾listset_difference_raw_nodup (`l) (`k) (proj2_sig l).
 
-Definition listset_union_raw (l k : list A) := listset_diff_raw l k ++ k.
+Definition listset_union_raw (l k : list A) := listset_difference_raw l k ++ k.
 Lemma listset_union_raw_in l k x : In x (listset_union_raw l k) ↔ In x l ∨ In x k.
 Proof. 
-  unfold listset_union_raw. rewrite in_app_iff, listset_diff_raw_in.
+  unfold listset_union_raw. rewrite in_app_iff, listset_difference_raw_in.
   intuition. case (decide (In x k)); intuition.
 Qed.
 Lemma listset_union_raw_nodup l k : NoDup l → NoDup k → NoDup (listset_union_raw l k).
 Proof.
   intros. apply NoDup_app.
-    now apply listset_diff_raw_nodup.
-   easy.
-  intro. rewrite listset_diff_raw_in. intuition.
+  * now apply listset_difference_raw_nodup.
+  * easy.
+  * intro. rewrite listset_difference_raw_in. intuition.
 Qed.
 Global Instance listset_union: Union (listset A) := λ l k,
   listset_union_raw (`l) (`k)↾listset_union_raw_nodup (`l) (`k) (proj2_sig l) (proj2_sig k).
 
-Fixpoint listset_inter_raw (l k : list A) :=
+Fixpoint listset_intersection_raw (l k : list A) :=
   match l with
   | [] => []
-  | x :: l => if decide_rel In x k then x :: listset_inter_raw l k else listset_inter_raw l k
+  | x :: l =>
+    if decide_rel In x k
+    then x :: listset_intersection_raw l k
+    else listset_intersection_raw l k
   end.
-Lemma listset_inter_raw_in l k x : In x (listset_inter_raw l k) ↔ In x l ∧ In x k.
-Proof. split; induction l; simpl; try case_decide; simpl; intuition congruence. Qed.
-Lemma listset_inter_raw_nodup l k : NoDup l → NoDup (listset_inter_raw l k).
+Lemma listset_intersection_raw_in l k x :
+  In x (listset_intersection_raw l k) ↔ In x l ∧ In x k.
+Proof.
+  split; induction l; simpl; try case_decide; simpl; intuition congruence.
+Qed.
+Lemma listset_intersection_raw_nodup l k :
+  NoDup l → NoDup (listset_intersection_raw l k).
 Proof.
   induction 1; simpl; try case_decide.
-    constructor.
-   constructor. rewrite listset_inter_raw_in; intuition. easy.
-  easy.
+  * constructor.
+  * constructor. rewrite listset_intersection_raw_in; intuition. easy.
+  * easy.
 Qed.
-Global Instance listset_inter: Intersection (listset A) := λ l k,
-  listset_inter_raw (`l) (`k)↾listset_inter_raw_nodup (`l) (`k) (proj2_sig l).
+Global Instance listset_intersection: Intersection (listset A) := λ l k,
+  listset_intersection_raw (`l) (`k)↾listset_intersection_raw_nodup (`l) (`k) (proj2_sig l).
 
-Definition listset_add_raw x (l : list A) : list A := if decide_rel In x l then l else x :: l.
+Definition listset_add_raw x (l : list A) : list A :=
+  if decide_rel In x l then l else x :: l.
 Lemma listset_add_raw_in x l y : In y (listset_add_raw x l) ↔ y = x ∨ In y l.
 Proof. unfold listset_add_raw. case (decide_rel _); firstorder congruence. Qed.
 Lemma listset_add_raw_nodup x l : NoDup l → NoDup (listset_add_raw x l).
@@ -75,9 +87,10 @@ Proof. induction l; simpl. constructor. now apply listset_add_raw_nodup. Qed.
 Lemma listset_map_raw_in f l x : In x (listset_map_raw f l) ↔ ∃ y, x = f y ∧ In y l.
 Proof.
   split.
-   induction l; simpl. easy. rewrite listset_add_raw_in. firstorder.
-  intros [?[??]]. subst. induction l; simpl in *. easy.
-  rewrite listset_add_raw_in. firstorder congruence.
+  * induction l; simpl; [easy |].
+    rewrite listset_add_raw_in. firstorder.
+  * intros [?[??]]. subst. induction l; simpl in *; [easy |].
+    rewrite listset_add_raw_in. firstorder congruence.
 Qed.
 Global Instance listset_map: Map A (listset A) := λ f l,
   listset_map_raw f (`l)↾listset_map_raw_nodup f (`l).
@@ -85,12 +98,12 @@ Global Instance listset_map: Map A (listset A) := λ f l,
 Global Instance: Collection A (listset A).
 Proof.
   split.
-       easy.
-      compute. intuition.
-     intros. apply listset_union_raw_in.
-    intros. apply listset_inter_raw_in.
-   intros. apply listset_diff_raw_in.
-  intros. apply listset_map_raw_in.
+  * easy.
+  * compute. intuition.
+  * intros. apply listset_union_raw_in.
+  * intros. apply listset_intersection_raw_in.
+  * intros. apply listset_difference_raw_in.
+  * intros. apply listset_map_raw_in.
 Qed.
 
 Global Instance listset_elems: Elements A (listset A) := @proj1_sig _ _.
diff --git a/theories/monads.v b/theories/monads.v
index 79e8efc8..62d6b392 100644
--- a/theories/monads.v
+++ b/theories/monads.v
@@ -15,5 +15,6 @@ Arguments mjoin {M MJoin A} _.
 Arguments fmap {M FMap A B} _ _.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
-Notation "x ← y ; z" := (y ≫= (λ x : _, z)) (at level 65, next at level 35, right associativity) : C_scope.
+Notation "x ← y ; z" := (y ≫= (λ x : _, z))
+  (at level 65, next at level 35, right associativity) : C_scope.
 Infix "<$>" := fmap (at level 65, right associativity, only parsing) : C_scope.
diff --git a/theories/nmap.v b/theories/nmap.v
index 05e638e5..03791529 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -23,7 +23,7 @@ Global Instance Npartial_alter: PartialAlter N Nmap := λ A f i t,
   end.
 Global Instance Ndom {A} : Dom N (Nmap A) := λ A _ _ _ t,
   match t with
-  | Build_Nmap o t => option_case (λ _, {{ 0 }}) ∅ o ∪ (Pdom_raw Npos (`t))
+  | Build_Nmap o t => option_case (λ _, {[ 0 ]}) ∅ o ∪ (Pdom_raw Npos (`t))
   end.
 Global Instance Nmerge: Merge Nmap := λ A f t1 t2,
   match t1, t2 with
@@ -37,16 +37,20 @@ Global Instance Nfmap: FMap Nmap := λ A B f t,
 Global Instance: FinMap N Nmap.
 Proof.
   split.
-        intros ? [??] [??] H. f_equal.
-         now apply (H 0).
-        apply finmap_eq. intros i. now apply (H (Npos i)).
-       now intros ? [|?].
-      intros ? f [? t] [|i]. easy. now apply (lookup_partial_alter f t i).
-     intros ? f [? t] [|i] [|j]; try intuition congruence.
-     intros. apply (lookup_partial_alter_ne f t i j). congruence.
-    intros ??? [??] []. easy. apply lookup_fmap.
-   intros ?? ???????? [o t] n; unfold dom, lookup, Ndom, Nlookup; simpl.
-   rewrite elem_of_union, Plookup_raw_dom.
-   destruct o, n; esimplify_elem_of (simplify_is_Some; eauto).
-  intros ? f ? [o1 t1] [o2 t2] [|?]. easy. apply (merge_spec f t1 t2).
+  * intros ? [??] [??] H. f_equal.
+    + now apply (H 0).
+    + apply finmap_eq. intros i. now apply (H (Npos i)).
+  * now intros ? [|?].
+  * intros ? f [? t] [|i].
+    + easy.
+    + now apply (lookup_partial_alter f t i).
+  * intros ? f [? t] [|i] [|j]; try intuition congruence.
+    intros. apply (lookup_partial_alter_ne f t i j). congruence.
+  * intros ??? [??] []. easy. apply lookup_fmap.
+  * intros ?? ???????? [o t] n; unfold dom, lookup, Ndom, Nlookup; simpl.
+    rewrite elem_of_union, Plookup_raw_dom.
+    destruct o, n; esimplify_elem_of (simplify_is_Some; eauto).
+  * intros ? f ? [o1 t1] [o2 t2] [|?].
+    + easy.
+    + apply (merge_spec f t1 t2).
 Qed.
diff --git a/theories/numbers.v b/theories/numbers.v
index 47834170..a3df40ef 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -1,6 +1,8 @@
 Require Export PArith NArith ZArith.
 Require Export base decidable fin_collections.
 
+Infix "≤" := le : nat_scope.
+
 Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
 Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec.
 Notation "(~0)" := xO (only parsing) : positive_scope.
@@ -41,18 +43,19 @@ Lemma Nmax_max `{FinCollection N C} X x : x ∈ X → (x ≤ Nmax X)%N.
 Proof.
   change ((λ b X, x ∈ X → (x ≤ b)%N) (collection_fold N.max 0%N X) X).
   apply collection_fold_ind.
-    solve_proper.
-   simplify_elem_of.
-  simplify_elem_of. apply N.le_max_l. apply N.max_le_iff; auto.
+  * solve_proper.
+  * simplify_elem_of.
+  * simplify_elem_of. apply N.le_max_l. apply N.max_le_iff; auto.
 Qed.
 
 Instance Nfresh `{FinCollection N C} : Fresh N C := λ l, (1 + Nmax l)%N.
 Instance Nfresh_spec `{FinCollection N C} : FreshSpec N C.
 Proof.
   split.
-   intros. unfold fresh, Nfresh.
-   setoid_replace X with Y; esimplify_elem_of.
-  intros X E. assert (1 ≤ 0)%N as []; [| easy].
-  apply N.add_le_mono_r with (Nmax X).
-  now apply Nmax_max.
+  * intros. unfold fresh, Nfresh.
+    setoid_replace X with Y; [easy |].
+    now apply elem_of_equiv.
+  * intros X E. assert (1 ≤ 0)%N as []; [| easy].
+    apply N.add_le_mono_r with (Nmax X).
+    now apply Nmax_max.
 Qed.
diff --git a/theories/option.v b/theories/option.v
index 3fbbf81a..7b7f7c0c 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -6,7 +6,7 @@ Lemma Some_ne_None `(a : A) : Some a ≠ None.
 Proof. congruence. Qed.
 Lemma eq_None_ne_Some `(x : option A) a : x = None → x ≠ Some a.
 Proof. congruence. Qed.
-Lemma Some_inj {A} (a b : A) : Some a = Some b → a = b.
+Instance Some_inj {A} : Injective (=) (=) (@Some A).
 Proof. congruence. Qed.
 
 Definition option_case {A B} (f : A → B) (b : B) (x : option A) :=
@@ -15,26 +15,33 @@ Definition option_case {A B} (f : A → B) (b : B) (x : option A) :=
   | Some a => f a
   end.
 
+Definition maybe {A} (a : A) (x : option A) :=
+  match x with
+  | None => a
+  | Some a => a
+  end.
+
 Lemma option_eq {A} (x y : option A) :
   x = y ↔ ∀ a, x = Some a ↔ y = Some a.
 Proof.
   split.
-   intros. now subst.
-  intros E. destruct x, y.
-     now apply E.
-    symmetry. now apply E.
-   now apply E.
-  easy.
+  * intros. now subst.
+  * intros E. destruct x, y.
+    + now apply E.
+    + symmetry. now apply E.
+    + now apply E.
+    + easy.
 Qed.
 
 Definition is_Some `(x : option A) := ∃ a, x = Some a.
 Hint Extern 10 (is_Some _) => solve [eexists; eauto].
 
-Ltac simplify_is_Some := repeat intro; repeat (
+Ltac simplify_is_Some := repeat intro; repeat
   match goal with
+  | _ => progress simplify_eqs
   | H : is_Some _ |- _ => destruct H as [??]
   | |- is_Some _ => eauto
-  end || simplify_eqs).
+  end.
 
 Lemma Some_is_Some `(a : A) : is_Some (Some a).
 Proof. simplify_is_Some. Qed.
@@ -56,14 +63,15 @@ Lemma make_eq_Some {A} (x : option A) a :
   is_Some x → (∀ b, x = Some b → b = a) → x = Some a.
 Proof. intros [??] H. subst. f_equal. auto. Qed.
 
-Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)} (x y : option A) : Decision (x = y) :=
+Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)} (x y : option A) :
+    Decision (x = y) :=
   match x with
   | Some a =>
     match y with
     | Some b =>
       match dec a b with
       | left H => left (f_equal _ H)
-      | right H => right (H ∘ Some_inj _ _)
+      | right H => right (H ∘ injective Some _ _)
       end
     | None => right (Some_ne_None _)
     end
@@ -87,7 +95,8 @@ Ltac option_lift_inv := repeat
 Lemma option_lift_inv_Some `(P : A → Prop) x : option_lift P (Some x) → P x.
 Proof. intros. now option_lift_inv. Qed.
 
-Definition option_lift_sig `(P : A → Prop) (x : option A) : option_lift P x → option (sig P) :=
+Definition option_lift_sig `(P : A → Prop) (x : option A) :
+    option_lift P x → option (sig P) :=
   match x with
   | Some a => λ p, Some (exist _ a (option_lift_inv_Some P a p))
   | None => λ _, None
@@ -104,16 +113,16 @@ Lemma option_lift_dsig_Some `(P : A → Prop) `{∀ x : A, Decision (P x)} x y p
   option_lift_dsig P x px = Some (y↾py) ↔ x = Some y.
 Proof.
   split.
-   destruct x; simpl; intros; now simplify_eqs.
-  intros. subst. simpl. f_equal. now apply dsig_eq.
+  * destruct x; simpl; intros; now simplify_eqs.
+  * intros. subst. simpl. f_equal. now apply dsig_eq.
 Qed.
 
 Lemma option_lift_dsig_is_Some `(P : A → Prop) `{∀ x : A, Decision (P x)} x px :
   is_Some (option_lift_dsig P x px) ↔ is_Some x.
 Proof.
   split.
-   intros [[??] ?]. eapply is_Some_2, option_lift_dsig_Some; eauto.
-  intros [??]. subst. eapply is_Some_2. reflexivity.
+  * intros [[??] ?]. eapply is_Some_2, option_lift_dsig_Some; eauto.
+  * intros [??]. subst. eapply is_Some_2. reflexivity.
 Qed.
 
 Instance option_ret: MRet option := @Some.
@@ -141,9 +150,11 @@ Ltac simplify_options := repeat
     simpl
   end.
 
-Lemma option_fmap_is_Some {A B} (f : A → B) (x : option A) : is_Some x ↔ is_Some (f <$> x).
+Lemma option_fmap_is_Some {A B} (f : A → B) (x : option A) :
+  is_Some x ↔ is_Some (f <$> x).
 Proof. destruct x; split; intros [??]; subst; compute; eauto; discriminate. Qed.
-Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) : x = None ↔ f <$> x = None.
+Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) :
+  x = None ↔ f <$> x = None.
 Proof. unfold fmap, option_fmap. destruct x; simpl; split; congruence. Qed.
 
 Instance option_union: UnionWith option := λ A f x y,
@@ -153,13 +164,19 @@ Instance option_union: UnionWith option := λ A f x y,
   | None, Some b => Some b
   | None, None => None
   end.
-Instance option_intersect: IntersectWith option := λ A f x y,
+Instance option_intersection: IntersectionWith option := λ A f x y,
   match x, y with
   | Some a, Some b => Some (f a b)
   | _, _ => None
   end.
+Instance option_difference: DifferenceWith 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_intersect.
+Section option_union_intersection.
   Context {A} (f : A → A → A).
 
   Global Instance: LeftId (=) None (union_with f).
@@ -172,4 +189,11 @@ Section option_union_intersect.
   Proof. intros ? [?|] [?|] [?|]; compute; try reflexivity. now rewrite (associative f). Qed.
   Global Instance: Idempotent (=) f → Idempotent (=) (union_with f).
   Proof. intros ? [?|]; compute; try reflexivity. now rewrite (idempotent f). Qed.
-End option_union_intersect.
+End option_union_intersection.
+
+Section option_difference.
+  Context {A} (f : A → A → option A).
+
+  Global Instance: RightId (=) None (difference_with f).
+  Proof. now intros [?|]. Qed.
+End option_difference.
diff --git a/theories/orders.v b/theories/orders.v
index cb31f3ce..9d164b9c 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -5,17 +5,24 @@ Section preorder.
 
   Global Instance preorder_equiv: Equiv A := λ X Y, X ⊆ Y ∧ Y ⊆ X.
   Instance preorder_equivalence: @Equivalence A (≡).
-  Proof. split. firstorder. firstorder. intros x y z; split; transitivity y; firstorder. Qed.
+  Proof.
+    split.
+    * firstorder.
+    * firstorder.
+    * intros x y z; split; transitivity y; firstorder.
+  Qed.
 
   Global Instance: Proper ((≡) ==> (≡) ==> iff) (⊆).
   Proof.
-    unfold equiv, preorder_equiv. intros x1 y1 ? x2 y2 ?. split; intro.
-     transitivity x1. tauto. transitivity x2; tauto.
-    transitivity y1. tauto. transitivity y2; tauto.
+    unfold equiv, preorder_equiv.
+    intros x1 y1 ? x2 y2 ?. split; intro.
+    * transitivity x1. tauto. transitivity x2; tauto.
+    * transitivity y1. tauto. transitivity y2; tauto.
   Qed.
 End preorder.
 
-Hint Extern 0 (@Equivalence _ (≡)) => class_apply preorder_equivalence : typeclass_instances.
+Hint Extern 0 (@Equivalence _ (≡)) =>
+  class_apply preorder_equivalence : typeclass_instances.
 
 Section bounded_join_sl.
   Context `{BoundedJoinSemiLattice A}.
@@ -40,7 +47,9 @@ Section bounded_join_sl.
   Proof. auto. Qed.
 
   Global Instance: Proper ((≡) ==> (≡) ==> (≡)) (∪).
-  Proof. unfold equiv, preorder_equiv. split; apply union_compat; simpl in *; tauto. Qed.
+  Proof.
+    unfold equiv, preorder_equiv. split; apply union_compat; simpl in *; tauto.
+  Qed.
   Global Instance: Idempotent (≡) (∪).
   Proof. split; eauto. Qed.
   Global Instance: LeftId (≡) ∅ (∪).
@@ -66,7 +75,8 @@ End bounded_join_sl.
 Section meet_sl.
   Context `{MeetSemiLattice A}.
 
-  Hint Resolve subseteq_intersection_l subseteq_intersection_r intersection_greatest.
+  Hint Resolve subseteq_intersection_l subseteq_intersection_r
+    intersection_greatest.
 
   Lemma intersection_compat_l x1 x2 y : x1 ⊆ x2 → x1 ∩ y ⊆ x2.
   Proof. intros. transitivity x1; auto. Qed.
@@ -84,7 +94,10 @@ Section meet_sl.
   Proof. auto. Qed.
 
   Global Instance: Proper ((≡) ==> (≡) ==> (≡)) (∩).
-  Proof. unfold equiv, preorder_equiv. split; apply intersection_compat; simpl in *; tauto. Qed.
+  Proof.
+    unfold equiv, preorder_equiv. split;
+      apply intersection_compat; simpl in *; tauto.
+  Qed.
   Global Instance: Idempotent (≡) (∩).
   Proof. split; eauto. Qed.
   Global Instance: Commutative (≡) (∩).
diff --git a/theories/pmap.v b/theories/pmap.v
index 924ec5b1..65897410 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -17,7 +17,8 @@ Inductive Pmap_raw A :=
 Arguments Pleaf {_}.
 Arguments Pnode {_} _ _ _.
 
-Instance Pmap_raw_eq_dec `{∀ x y : A, Decision (x = y)} : ∀ x y : Pmap_raw A, Decision (x = y).
+Instance Pmap_raw_eq_dec `{∀ x y : A, Decision (x = y)} (x y : Pmap_raw A) :
+  Decision (x = y).
 Proof. solve_decision. Defined.
 
 Inductive Pmap_ne {A} : Pmap_raw A → Prop :=
@@ -29,36 +30,41 @@ Local Hint Constructors Pmap_ne.
 Instance Pmap_ne_dec `(t : Pmap_raw A) : Decision (Pmap_ne t).
 Proof.
   red. induction t as [|? IHl [?|] ? IHr].
-    right. now inversion 1.
-   now intuition.
-  destruct IHl, IHr; try solve [left; auto]; right; inversion_clear 1; contradiction.
+  * right. now inversion 1.
+  * now intuition.
+  * destruct IHl, IHr; try solve [left; auto]; right;
+      inversion_clear 1; contradiction.
 Qed.
 
 Inductive Pmap_wf {A} : Pmap_raw A → Prop :=
   | Pmap_wf_leaf : Pmap_wf Pleaf
   | Pmap_wf_node l x r : Pmap_wf l → Pmap_wf r → Pmap_wf (Pnode l (Some x) r)
-  | Pmap_wf_empty l r : Pmap_wf l → Pmap_wf r → (Pmap_ne l ∨ Pmap_ne r) → Pmap_wf (Pnode l None r).
+  | Pmap_wf_empty l r :
+     Pmap_wf l → Pmap_wf r → (Pmap_ne l ∨ Pmap_ne r) → Pmap_wf (Pnode l None r).
 Local Hint Constructors Pmap_wf.
 
 Instance Pmap_wf_dec `(t : Pmap_raw A) : Decision (Pmap_wf t).
 Proof.
   red. induction t as [|l IHl [?|] r IHr]; simpl.
-    intuition.
-   destruct IHl, IHr; try solve [left; intuition]; right; inversion_clear 1; intuition.
-  destruct IHl, IHr, (decide (Pmap_ne l)), (decide (Pmap_ne r)); 
-    try solve [left; intuition]; right; inversion_clear 1; intuition.
+  * intuition.
+  * destruct IHl, IHr; try solve [left; intuition];
+      right; inversion_clear 1; intuition.
+  * destruct IHl, IHr, (decide (Pmap_ne l)), (decide (Pmap_ne r)); 
+      try solve [left; intuition]; right; inversion_clear 1; intuition.
 Qed.
 
 Definition Pmap A := @dsig (Pmap_raw A) Pmap_wf _.
 
-Global Instance Pmap_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Pmap A) : Decision (t1 = t2) :=
+Global Instance Pmap_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Pmap A) :
+    Decision (t1 = t2) :=
   match Pmap_raw_eq_dec (`t1) (`t2) with
   | left H => left (dsig_eq _ t1 t2 H)
   | right H => right (H ∘ eq_ind _ (λ x, `t1 = `x) eq_refl _)
   end.
 
 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.
+Global Instance Pempty {A} : Empty (Pmap A) :=
+  (∅ : Pmap_raw A)↾bool_decide_pack _ Pmap_wf_leaf.
 
 Instance Plookup_raw: Lookup positive Pmap_raw :=
   fix Plookup_raw A (i : positive) (t : Pmap_raw A) {struct t} : option A :=
@@ -79,39 +85,40 @@ Proof. now destruct i. Qed.
 Lemma Pmap_ne_lookup `(t : Pmap_raw A) : Pmap_ne t → ∃ i x, t !! i = Some x.
 Proof.
   induction 1 as [? x ?| l r ? IHl | l r ? IHr].
-    intros. now exists 1 x.
-   destruct IHl as [i [x ?]]. now exists (i~0) x.
-  destruct IHr as [i [x ?]]. now exists (i~1) x.
+  * intros. now exists 1 x.
+  * destruct IHl as [i [x ?]]. now exists (i~0) x.
+  * destruct IHr as [i [x ?]]. now exists (i~1) x.
 Qed.
 
 Lemma Pmap_wf_eq_get {A} (t1 t2 : Pmap_raw A) :
   Pmap_wf t1 → Pmap_wf t2 → (∀ i, t1 !! i = t2 !! i) → t1 = t2.
 Proof.
-  intros t1wf. revert t2. induction t1wf as [| ? x ? ? IHl ? IHr | l r ? IHl ? IHr Hne1 ].
-    destruct 1 as [| | ???? [?|?]]; intros Hget.
-       easy.
-      discriminate (Hget 1).
-     destruct (Pmap_ne_lookup l) as [i [??]]; auto.
-     specialize (Hget (i~0)). simpl in *. congruence.
-    destruct (Pmap_ne_lookup r) as [i [??]]; auto.
-    specialize (Hget (i~1)). simpl in *. congruence.
-   destruct 1; intros Hget.
-     discriminate (Hget xH).
-    f_equal.
-      apply IHl; auto. intros i. now apply (Hget (i~0)).
-     now apply (Hget 1).
-    apply IHr; auto. intros i. now apply (Hget (i~1)).
-   specialize (Hget 1). simpl in *. congruence.
-  destruct 1; intros Hget.
-    destruct Hne1.
-     destruct (Pmap_ne_lookup l) as [i [??]]; auto.
-     specialize (Hget (i~0)). simpl in *. congruence.
-    destruct (Pmap_ne_lookup r) as [i [??]]; auto.
-    specialize (Hget (i~1)). simpl in *. congruence.
-   specialize (Hget 1). simpl in *. congruence.
-  f_equal.
-   apply IHl; auto. intros i. now apply (Hget (i~0)).
-  apply IHr; auto. intros i. now apply (Hget (i~1)).
+  intros t1wf. revert t2.
+  induction t1wf as [| ? x ? ? IHl ? IHr | l r ? IHl ? IHr Hne1 ].
+  * destruct 1 as [| | ???? [?|?]]; intros Hget.
+    + easy.
+    + discriminate (Hget 1).
+    + destruct (Pmap_ne_lookup l) as [i [??]]; auto.
+      specialize (Hget (i~0)). simpl in *. congruence.
+    + destruct (Pmap_ne_lookup r) as [i [??]]; auto.
+      specialize (Hget (i~1)). simpl in *. congruence.
+  * destruct 1; intros Hget.
+    + discriminate (Hget xH).
+    + f_equal.
+      - apply IHl; auto. intros i. now apply (Hget (i~0)).
+      - now apply (Hget 1).
+      - apply IHr; auto. intros i. now apply (Hget (i~1)).
+    + specialize (Hget 1). simpl in *. congruence.
+  * destruct 1; intros Hget.
+    + destruct Hne1.
+      destruct (Pmap_ne_lookup l) as [i [??]]; auto.
+      - specialize (Hget (i~0)). simpl in *. congruence.
+      - destruct (Pmap_ne_lookup r) as [i [??]]; auto.
+        specialize (Hget (i~1)). simpl in *. congruence.
+    + specialize (Hget 1). simpl in *. congruence.
+    + f_equal.
+      - apply IHl; auto. intros i. now apply (Hget (i~0)).
+      - apply IHr; auto. intros i. now apply (Hget (i~1)).
 Qed.
 
 Fixpoint Psingleton_raw {A} (i : positive) (x : A) : Pmap_raw A :=
@@ -130,7 +137,8 @@ Local Hint Resolve Psingleton_raw_wf.
 
 Lemma Plookup_raw_singleton {A} i (x : A) : Psingleton_raw i x !! i = Some x.
 Proof. now induction i. Qed.
-Lemma Plookup_raw_singleton_ne {A} i j (x : A) : i ≠ j → Psingleton_raw i x !! j = None.
+Lemma Plookup_raw_singleton_ne {A} i j (x : A) :
+  i ≠ j → Psingleton_raw i x !! j = None.
 Proof. revert j. induction i; intros [?|?|]; simpl; auto. congruence. Qed.
 
 Definition Pnode_canon `(l : Pmap_raw A) (o : option A) (r : Pmap_raw A) :=
@@ -154,10 +162,13 @@ Lemma Pnode_canon_lookup_xI `(l : Pmap_raw A) (o : option A) (r : Pmap_raw A) i
   Pnode_canon l o r !! i~1 = r !! i.
 Proof. now destruct l,o,r. Qed.
 Ltac Pnode_canon_rewrite := repeat (
-  rewrite Pnode_canon_lookup_xH || rewrite Pnode_canon_lookup_xO || rewrite Pnode_canon_lookup_xI).
+  rewrite Pnode_canon_lookup_xH ||
+  rewrite Pnode_canon_lookup_xO ||
+  rewrite Pnode_canon_lookup_xI).
 
 Instance Ppartial_alter_raw: PartialAlter positive Pmap_raw :=
-  fix Ppartial_alter_raw A (f : option A → option A) (i : positive) (t : Pmap_raw A) {struct t} : Pmap_raw A :=
+  fix Ppartial_alter_raw A (f : option A → option A) (i : positive)
+    (t : Pmap_raw A) {struct t} : Pmap_raw A :=
   match t with
   | Pleaf =>
     match f None with
@@ -172,39 +183,43 @@ Instance Ppartial_alter_raw: PartialAlter positive Pmap_raw :=
     end
   end.
 
-Lemma Ppartial_alter_raw_wf {A} f i (t : Pmap_raw A) : Pmap_wf t → Pmap_wf (partial_alter f i t).
+Lemma Ppartial_alter_raw_wf {A} f i (t : Pmap_raw A) :
+  Pmap_wf t → Pmap_wf (partial_alter f i t).
 Proof.
   intros twf. revert i. induction twf.
-    unfold partial_alter. simpl. case (f None); intuition.
-   intros [?|?|]; simpl; intuition.
-  intros [?|?|]; simpl; intuition.
+  * unfold partial_alter. simpl. case (f None); intuition.
+  * intros [?|?|]; simpl; intuition.
+  * intros [?|?|]; simpl; intuition.
 Qed.
 
 Global Instance Ppartial_alter: PartialAlter positive 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) : partial_alter f i t !! i = f (t !! i).
+Lemma Plookup_raw_alter {A} f i (t : Pmap_raw A) :
+  partial_alter f i t !! i = f (t !! i).
 Proof.
   revert i. induction t.
-   simpl. case (f None).
-    intros. now apply Plookup_raw_singleton.
-   now destruct i.
-  intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
+  * simpl. case (f None).
+    + intros. now apply Plookup_raw_singleton.
+    + now destruct i.
+  * intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
 Qed.
-Lemma Plookup_raw_alter_ne {A} f i j (t : Pmap_raw A) : i ≠ j → partial_alter f i t !! j = t !! j.
+Lemma Plookup_raw_alter_ne {A} f i j (t : Pmap_raw A) :
+  i ≠ j → partial_alter f i t !! j = t !! j.
 Proof.
   revert i j. induction t as [|l IHl ? r IHr].
-   simpl. intros. case (f None).
-    intros. now apply Plookup_raw_singleton_ne.
-   easy.
-  intros [?|?|] [?|?|]; simpl; Pnode_canon_rewrite; auto; congruence.
+  * simpl. intros. case (f None).
+    + intros. now apply Plookup_raw_singleton_ne.
+    + easy.
+  * intros [?|?|] [?|?|]; simpl; Pnode_canon_rewrite; auto; congruence.
 Qed.
 
 Instance Pfmap_raw: FMap Pmap_raw :=
   fix Pfmap_raw A B f (t : Pmap_raw A) : Pmap_raw B :=
   match t with
   | Pleaf => Pleaf
-  | Pnode l x r => Pnode (@fmap _ Pfmap_raw _ _ f l) (fmap f x) (@fmap _ Pfmap_raw _ _ f r)
+  | Pnode l x r =>
+    Pnode (@fmap _ Pfmap_raw _ _ f l) (fmap f x) (@fmap _ Pfmap_raw _ _ f r)
   end.
 
 Lemma Pfmap_raw_ne `(f : A → B) (t : Pmap_raw A) : Pmap_ne t → Pmap_ne (fmap f t).
@@ -213,9 +228,11 @@ Local Hint Resolve Pfmap_raw_ne.
 Lemma Pfmap_raw_wf `(f : A → B) (t : Pmap_raw A) : Pmap_wf t → Pmap_wf (fmap f t).
 Proof. induction 1; simpl; intuition auto. Qed. 
 
-Global Instance Pfmap: FMap Pmap := λ A B f t, dexist _ (Pfmap_raw_wf f _ (proj2_dsig t)).
+Global Instance Pfmap: FMap Pmap := λ A B f t,
+  dexist _ (Pfmap_raw_wf f _ (proj2_dsig t)).
 
-Lemma Plookup_raw_fmap `(f : A → B) (t : Pmap_raw A) i : fmap f t !! i = fmap f (t !! i).
+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. easy. intros [?|?|]; simpl; auto. Qed.
 
 Section dom.
@@ -224,16 +241,19 @@ Section dom.
   Fixpoint Pdom_raw (f : positive → B) `(t : Pmap_raw A) : D :=
     match t with
     | Pleaf => ∅
-    | Pnode l o r => option_case (λ _, {{ f 1 }}) ∅ o ∪ Pdom_raw (f ∘ (~0)) l ∪ Pdom_raw (f ∘ (~1)) r
+    | Pnode l o r => option_case (λ _, {[ f 1 ]}) ∅ o
+                       ∪ Pdom_raw (f ∘ (~0)) l ∪ Pdom_raw (f ∘ (~1)) r
     end.
 
-  Lemma Plookup_raw_dom f `(t : Pmap_raw A) x : x ∈ Pdom_raw f t ↔ ∃ i, x = f i ∧ is_Some (t !! i).
+  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]; esimplify_elem_of.
-    intros [i [? Hlookup]]; subst. revert f i Hlookup.
-    induction t as [|? IHl [?|] ? IHr]; intros f [?|?|];
-      simplify_elem_of (now apply (IHl (f ∘ (~0))) || now apply (IHr (f ∘ (~1))) || simplify_is_Some).
+    * revert f. induction t as [|? IHl [?|] ? IHr]; esimplify_elem_of.
+    * intros [i [? Hlookup]]; subst. revert f i Hlookup.
+      induction t as [|? IHl [?|] ? IHr]; intros f [?|?|];
+        simplify_elem_of (now apply (IHl (f ∘ (~0))) 
+        || now apply (IHr (f ∘ (~1))) || simplify_is_Some).
   Qed.
 End dom.
 
@@ -246,14 +266,16 @@ Fixpoint Pmerge_aux `(f : option A → option B) (t : Pmap_raw A) : Pmap_raw B :
   end.
 Local Hint Constructors option_lift.
 
-Lemma Pmerge_aux_wf `(f : option A → option B) (t : Pmap_raw A) : Pmap_wf t → Pmap_wf (Pmerge_aux f t).
+Lemma Pmerge_aux_wf `(f : option A → option B) (t : Pmap_raw A) :
+  Pmap_wf t → Pmap_wf (Pmerge_aux f t).
 Proof. induction 1; simpl; auto. Qed.
 Local Hint Resolve Pmerge_aux_wf.
 
-Lemma Pmerge_aux_spec `(f : option A → option B) (Hf : f None = None) (t : Pmap_raw A) i :
+Lemma Pmerge_aux_spec `(f : option A → option B) (Hf : f None = None)
+    (t : Pmap_raw A) i :
   Pmerge_aux f t !! i = f (t !! i).
 Proof.
-  revert i. induction t as [| l IHl o r IHr ]; auto.
+  revert i. induction t as [| l IHl o r IHr ]; [easy |].
   intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
 Qed.
 
@@ -267,7 +289,8 @@ Global Instance Pmerge_raw: Merge Pmap_raw :=
   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).
+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,
   dexist (merge f (`t1) (`t2)) (Pmerge_wf _ _ _ (proj2_dsig t1) (proj2_dsig t2)).
@@ -276,24 +299,24 @@ Lemma Pmerge_raw_spec {A} f (Hf : f None None = None) (t1 t2 : Pmap_raw A) i :
   merge f t1 t2 !! i = f (t1 !! i) (t2 !! i).
 Proof.
   revert t2 i. induction t1 as [| l1 IHl1 o1 r1 IHr1 ].
-   simpl. now apply Pmerge_aux_spec.
-  destruct t2 as [| l2 o2 r2 ].
-   unfold merge, Pmerge_raw. intros. now rewrite Pmerge_aux_spec.
-  intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
+  * simpl. now apply Pmerge_aux_spec.
+  * destruct t2 as [| l2 o2 r2 ].
+    + unfold merge, Pmerge_raw. intros. now rewrite Pmerge_aux_spec.
+    + intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
 Qed.
 
 Global Instance: FinMap positive Pmap.
 Proof.
   split.
-        intros ? [t1?] [t2?]. intros. apply dsig_eq. simpl.
-        apply Pmap_wf_eq_get; auto; now apply (bool_decide_unpack _).
-       now destruct i.
-      intros ?? [??] ?. now apply Plookup_raw_alter.
-     intros ?? [??] ??. now apply Plookup_raw_alter_ne.
-    intros ??? [??]. now apply Plookup_raw_fmap.
-   intros ?????????? [??] i. unfold dom, Pdom.
-   rewrite Plookup_raw_dom. unfold id. split.
-    intros [? [??]]. now subst.
-   firstorder.
-  intros ??? [??] [??] ?. now apply Pmerge_raw_spec.
+  * intros ? [t1?] [t2?]. intros. apply dsig_eq. simpl.
+    apply Pmap_wf_eq_get; auto; now apply (bool_decide_unpack _).
+  * now destruct i.
+  * intros ?? [??] ?. now apply Plookup_raw_alter.
+  * intros ?? [??] ??. now apply Plookup_raw_alter_ne.
+  * intros ??? [??]. now apply Plookup_raw_fmap.
+  * intros ?????????? [??] i. unfold dom, Pdom.
+    rewrite Plookup_raw_dom. unfold id. split.
+    + intros [? [??]]. now subst.
+    + firstorder.
+  * intros ??? [??] [??] ?. now apply Pmerge_raw_spec.
 Qed.
diff --git a/theories/subset.v b/theories/subset.v
index bf41e429..27662375 100644
--- a/theories/subset.v
+++ b/theories/subset.v
@@ -6,8 +6,8 @@ Instance subset_elem_of {A} : ElemOf A (subset A) | 100 := λ x P, P x.
 Instance subset_empty {A} : Empty (subset A) := λ _, False.
 Instance subset_singleton {A} : Singleton A (subset A) := (=).
 Instance subset_union {A} : Union (subset A) := λ P Q x, P x ∨ Q x.
-Instance subset_inter {A} : Intersection (subset A) := λ P Q x, P x ∧ Q x.
-Instance subset_diff {A} : Difference (subset A) := λ P Q x, P x ∧ ¬Q x.
+Instance subset_intersection {A} : Intersection (subset A) := λ P Q x, P x ∧ Q x.
+Instance subset_difference {A} : Difference (subset A) := λ P Q x, P x ∧ ¬Q x.
 Instance subset_map {A} : Map A (subset A) := λ f P x, ∃ y, f y = x ∧ P y.
 
 Instance subset_container: Collection A (subset A) | 100.
diff --git a/theories/trs.v b/theories/trs.v
index efb65063..17f79db5 100644
--- a/theories/trs.v
+++ b/theories/trs.v
@@ -3,19 +3,29 @@ Require Export base.
 Definition red `(R : relation A) (x : A) := ∃ y, R x y.
 Definition nf `(R : relation A) (x : A) := ¬red R x.
 
+(* The reflexive transitive closure *)
 Inductive rtc `(R : relation A) : relation A :=
   | rtc_refl x : rtc R x x
   | rtc_l x y z : R x y → rtc R y z → rtc R x z.
+(* A reduction of exactly n steps *)
 Inductive nsteps `(R : relation A) : nat → relation A :=
   | nsteps_O x : nsteps R 0 x x
   | nsteps_l n x y z : R x y → nsteps R n y z → nsteps R (S n) x z.
+(* A reduction whose length is bounded by n *)
+Inductive bsteps `(R : relation A) : nat → relation A :=
+  | bsteps_refl n x : bsteps R n x x
+  | bsteps_l n x y z : R x y → bsteps R n y z → bsteps R (S n) x z.
+(* The transitive closure *)
 Inductive tc `(R : relation A) : relation A :=
   | tc_once x y : R x y → tc R x y
   | tc_l x y z : R x y → tc R y z → tc R x z.
-Hint Constructors rtc nsteps tc : trs.
+
+Hint Constructors rtc nsteps bsteps tc : trs.
 
 Arguments rtc_l {_ _ _ _ _} _ _.
 Arguments nsteps_l {_ _ _ _ _ _} _ _.
+Arguments bsteps_refl {_ _} _ _.
+Arguments bsteps_l {_ _ _ _ _ _} _ _.
 Arguments tc_once {_ _ _} _ _.
 Arguments tc_l {_ _ _ _ _} _ _.
 
@@ -55,9 +65,9 @@ Section rtc.
     (Prefl : ∀ x, P x x) (Pstep : ∀ x y z, rtc R x y → R y z → P x y → P x z) :
     ∀ y z, rtc R y z → P y z.
   Proof.
-    assert (∀ y z, rtc R y z → ∀ x, rtc R x y → P x y → P x z).
-     induction 1; eauto using rtc_r.
-    eauto using rtc_refl.
+    cut (∀ y z, rtc R y z → ∀ x, rtc R x y → P x y → P x z).
+    { eauto using rtc_refl. }
+    induction 1; eauto using rtc_r.
   Qed.
 
   Lemma rtc_inv_r {x z} : rtc R x z → x = z ∨ ∃ y, rtc R x y ∧ R y z.
@@ -75,6 +85,31 @@ Section rtc.
   Lemma rtc_nsteps {x y} : rtc R x y → ∃ n, nsteps R n x y.
   Proof. induction 1; firstorder eauto with trs. Qed.
 
+  Lemma bsteps_once {n x y} : R x y → bsteps R (S n) x y.
+  Proof. eauto with trs. Qed.
+  Lemma bsteps_plus_r {n m x y} :
+    bsteps R n x y → bsteps R (n + m) x y.
+  Proof. induction 1; simpl; eauto with trs. Qed.
+  Lemma bsteps_weaken {n m x y} :
+    n ≤ m → bsteps R n x y → bsteps R m x y.
+  Proof.
+    intros. rewrite (Minus.le_plus_minus n m); auto using bsteps_plus_r.
+  Qed.
+  Lemma bsteps_plus_l {n m x y} :
+    bsteps R n x y → bsteps R (m + n) x y.
+  Proof. apply bsteps_weaken. auto with arith. Qed.
+  Lemma bsteps_S {n x y} :  bsteps R n x y → bsteps R (S n) x y.
+  Proof. apply bsteps_weaken. auto with arith. Qed.
+  Lemma bsteps_trans {n m x y z} :
+    bsteps R n x y → bsteps R m y z → bsteps R (n + m) x z.
+  Proof. induction 1; simpl; eauto using bsteps_plus_l with trs. Qed.
+  Lemma bsteps_r {n x y z} : bsteps R n x y → R y z → bsteps R (S n) x z.
+  Proof. induction 1; eauto with trs. Qed.
+  Lemma bsteps_rtc {n x y} : bsteps R n x y → rtc R x y.
+  Proof. induction 1; eauto with trs. Qed.
+  Lemma rtc_bsteps {x y} : rtc R x y → ∃ n, bsteps R n x y.
+  Proof. induction 1. exists 0. auto with trs. firstorder eauto with trs. Qed.
+
   Global Instance tc_trans: Transitive (tc R).
   Proof. red; induction 1; eauto with trs. Qed.
   Lemma tc_r {x y z} : tc R x y → R y z → tc R x z.
@@ -96,14 +131,11 @@ Section subrel.
   Proof. intros H1 H2. destruct H1. now apply red_subrel. Qed.
 
   Global Instance rtc_subrel: subrelation (rtc R1) (rtc R2).
-  Proof.
-    induction 1; [easy |].
-    eapply rtc_l; [eapply Hsub|]; eauto.
-  Qed.
+  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
+  Global Instance nsteps_subrel: subrelation (nsteps R1 n) (nsteps R2 n).
+  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
+  Global Instance bsteps_subrel: subrelation (bsteps R1 n) (bsteps R2 n).
+  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
   Global Instance tc_subrel: subrelation (tc R1) (tc R2).
-  Proof.
-    induction 1.
-     now apply tc_once, Hsub.
-    eapply tc_l; [eapply Hsub|]; eauto.
-  Qed.
+  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
 End subrel.
-- 
GitLab