diff --git a/theories/base.v b/theories/base.v
index 709d29b590c78028cc6fd6cea87bf7318133f612..e07bc30ac0006877cb60e363e9ec4c33c1eb00b0 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -266,6 +266,22 @@ Class Filter A B :=
 
 (* Arguments filter {_ _ _} _ {_} !_ / : simpl nomatch. *)
 
+(** We define variants of the relations [(â‰¡)] and [(âŠ†)] that are indexed by
+an environment. *)
+Class EquivEnv A B := equiv_env : A â†’ relation B.
+Notation "X â‰¡@{ E } Y" := (equiv_env E X Y)
+  (at level 70, format "X  â‰¡@{ E }  Y") : C_scope.
+Notation "(â‰¡@{ E } )" := (equiv_env E)
+  (E at level 1, only parsing) : C_scope.
+Instance: Params (@equiv_env) 4.
+
+Class SubsetEqEnv A B := subseteq_env : A â†’ relation B.
+Notation "X âŠ†@{ E } Y" := (subseteq_env E X Y)
+  (at level 70, format "X  âŠ†@{ E }  Y") : C_scope.
+Notation "(âŠ†@{ E } )" := (subseteq_env E)
+  (E at level 1, only parsing) : C_scope.
+Instance: Params (@subseteq_env) 4.
+
 (** ** Monadic operations *)
 (** We define operational type classes for the monadic operations bind, join 
 and fmap. These type classes are defined in a non-standard way by taking the
@@ -282,7 +298,7 @@ in the appropriate way, and so that it can be used for mutual recursion
 (the mapped function [f] is not part of the fixpoint) as well. This is a hack,
 and should be replaced by something more appropriate in future versions. *)
 
-(* We use these type classes merely for convenient overloading of notations and
+(** We use these type classes merely for convenient overloading of notations and
 do not formalize any theory on monads (we do not even define a class with the
 monad laws). *)
 Class MRet (M : Type â†’ Type) := mret: âˆ€ {A}, A â†’ M A.
@@ -316,11 +332,12 @@ Class MGuard (M : Type â†’ Type) :=
   mguard: âˆ€ P {dec : Decision P} {A}, M A â†’ M A.
 Notation "'guard' P ; o" := (mguard P o)
   (at level 65, only parsing, next at level 35, right associativity) : C_scope.
+Arguments mguard _ _ _ !_ _ !_ / : simpl nomatch.
 
 (** ** Operations on maps *)
 (** In this section we define operational type classes for the operations
 on maps. In the file [fin_maps] we will axiomatize finite maps.
-The function lookup [m !! k] should yield the element at key [k] in [m]. *)
+The function look up [m !! k] should yield the element at key [k] in [m]. *)
 Class Lookup (K A M : Type) :=
   lookup: K â†’ M â†’ option A.
 Instance: Params (@lookup) 4.
diff --git a/theories/list.v b/theories/list.v
index 97509a7c394d78d6f6dfc24439ce17641754ff0e..5447d05cc5aea32eea57bd9c3b7cbf9e7e19a65a 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -29,8 +29,9 @@ Notation "(++)" := app (only parsing) : C_scope.
 Notation "( l ++)" := (app l) (only parsing) : C_scope.
 Notation "(++ k )" := (Î» l, app l k) (only parsing) : C_scope.
 
-(** * General definitions *)
-(** Looking up, updating, and deleting elements of a list. *)
+(** * Definitions *)
+(** The operation [l !! i] gives the [i]th element of the list [l], or [None]
+in case [i] is out of bounds. *)
 Instance list_lookup {A} : Lookup nat A (list A) :=
   fix go (i : nat) (l : list A) {struct l} : option A :=
   match l with
@@ -41,6 +42,9 @@ Instance list_lookup {A} : Lookup nat A (list A) :=
     | S i => @lookup _ _ _ go i l
     end
   end.
+
+(** The operation [alter f i l] applies the function [f] to the [i]th element
+of [l]. In case [i] is out of bounds, the list is returned unchanged. *)
 Instance list_alter {A} (f : A â†’ A) : AlterD nat A (list A) f :=
   fix go (i : nat) (l : list A) {struct l} :=
   match l with
@@ -51,6 +55,10 @@ Instance list_alter {A} (f : A â†’ A) : AlterD nat A (list A) f :=
     | S i => x :: @alter _ _ _ f go i l
     end
   end.
+
+(** The operation [delete i l] removes the [i]th element of [l] and moves
+all consecutive elements one position ahead. In case [i] is out of bounds,
+the list is returned unchanged. *)
 Instance list_delete {A} : Delete nat (list A) :=
   fix go (i : nat) (l : list A) {struct l} : list A :=
   match l with
@@ -61,11 +69,14 @@ Instance list_delete {A} : Delete nat (list A) :=
     | S i => x :: @delete _ _ go i l
     end
   end.
+
+(** The operation [<[i:=x]> l] overwrites the element at position [i] with the
+value [x]. In case [i] is out of bounds, the list is returned unchanged. *)
 Instance list_insert {A} : Insert nat A (list A) := Î» i x,
   alter (Î» _, x) i.
 
-(** The function [option_list] converts an element of the option type into
-the empty list or a singleton list. *)
+(** The function [option_list o] converts an element [Some x] into the
+singleton list [[x]], and [None] into the empty list [[]]. *)
 Definition option_list {A} : option A â†’ list A := option_rect _ (Î» x, [x]) [].
 
 (** The function [filter P l] returns the list of elements of [l] that
@@ -105,6 +116,77 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
   end.
 Arguments resize {_} !_ _ !_.
 
+(** Functions to fold over a list. We redefine [foldl] with the arguments in
+the same order as in Haskell. *)
+Notation foldr := fold_right.
+
+Definition foldl {A B} (f : A â†’ B â†’ A) : A â†’ list B â†’ A :=
+  fix go a l :=
+  match l with
+  | [] => a
+  | x :: l => go (f a x) l
+  end.
+
+(** The monadic operations. *)
+Instance list_ret: MRet list := Î» A x, x :: @nil A.
+Instance list_fmap {A B} (f : A â†’ B) : FMapD list f :=
+  fix go (l : list A) :=
+  match l with
+  | [] => []
+  | x :: l => f x :: @fmap _ _ _ f go l
+  end.
+Instance list_bind {A B} (f : A â†’ list B) : MBindD list f :=
+  fix go (l : list A) :=
+  match l with
+  | [] => []
+  | x :: l => f x ++ @mbind _ _ _ f go l
+  end.
+Instance list_join: MJoin list :=
+  fix go A (ls : list (list A)) : list A :=
+  match ls with
+  | [] => []
+  | l :: ls => l ++ @mjoin _ go _ ls
+  end.
+
+(** We define stronger variants of map and fold that allow the mapped
+function to use the index of the elements. *)
+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.
+
+Definition ifoldr {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.
+
+(** Zipping lists. *)
+Definition zip_with {A B C} (f : A â†’ B â†’ C) : list A â†’ list B â†’ list C :=
+  fix go l1 l2 :=
+  match l1, l2 with
+  | x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2
+  | _ , _ => []
+  end.
+Notation zip := (zip_with pair).
+
+(** The function [permutations l] yields all permutations of [l]. *)
+Fixpoint interleave {A} (x : A) (l : list A) : list (list A) :=
+  match l with
+  | [] => [ [x] ]
+  | y :: l => (x :: y :: l) :: ((y ::) <$> interleave x l)
+  end.
+Fixpoint permutations {A} (l : list A) : list (list A) :=
+  match l with
+  | [] => [ [] ]
+  | x :: l => permutations l â‰«= interleave x
+  end.
+
 (** The predicate [suffix_of] holds if the first list is a suffix of the second.
 The predicate [prefix_of] holds if the first list is a prefix of the second. *)
 Definition suffix_of {A} : relation (list A) := Î» l1 l2, âˆƒ k, l2 = k ++ l1.
@@ -139,7 +221,14 @@ Inductive sublist {A} : relation (list A) :=
   | sublist_cons x l1 l2 : sublist l1 l2 â†’ sublist (x :: l1) (x :: l2)
   | sublist_cons_skip x l1 l2 : sublist l1 l2 â†’ sublist l1 (x :: l2).
 
-(** * Tactics on lists *)
+(** The [same_length] view allows convenient induction over two lists with the
+same length. *)
+Inductive same_length {A B} : 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).
+
+(** * Basic tactics on lists *)
 (** The tactic [discriminate_list_equality] discharges a goal if it contains
 a list equality involving [(::)] and [(++)] of two lists that have a different
 length as one of its hypotheses. *)
@@ -398,6 +487,7 @@ Lemma delete_middle (l1 l2 : list A) x :
   delete (length l1) (l1 ++ x :: l2) = l1 ++ l2.
 Proof. induction l1; simpl; f_equal; auto. Qed.
 
+(** ** Properties of the [elem_of] predicate *)
 Lemma not_elem_of_nil (x : A) : x âˆ‰ [].
 Proof. by inversion 1. Qed.
 Lemma elem_of_nil (x : A) : x âˆˆ [] â†” False.
@@ -472,6 +562,7 @@ Proof.
     elem_of_list_lookup_1, elem_of_list_lookup_2.
 Qed.
 
+(** ** Properties of the [NoDup] predicate *)
 Lemma NoDup_nil : NoDup (@nil A) â†” True.
 Proof. split; constructor. Qed.
 Lemma NoDup_cons (x : A) l : NoDup (x :: l) â†” x âˆ‰ l âˆ§ NoDup l.
@@ -491,7 +582,14 @@ Proof.
     setoid_rewrite elem_of_nil. naive_solver.
   * rewrite !NoDup_cons.
     setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app.
+split.
+destruct IHl.
+intros [??].
+split.
+    naive_solver.
+
     naive_solver.
+naive_solver.
 Qed.
 
 Global Instance NoDup_proper:
@@ -562,6 +660,7 @@ Section remove_dups.
   Qed.
 End remove_dups.
 
+(** ** Properties of the [filter] function *)
 Lemma elem_of_list_filter `{âˆ€ x : A, Decision (P x)} l x :
   x âˆˆ filter P l â†” P x âˆ§ x âˆˆ l.
 Proof.
@@ -575,6 +674,7 @@ Proof.
     rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto.
 Qed.
 
+(** ** Properties of the [reverse] function *)
 Lemma reverse_nil : reverse [] = @nil A.
 Proof. done. Qed.
 Lemma reverse_singleton (x : A) : reverse [x] = [x].
@@ -591,6 +691,7 @@ Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
 Lemma reverse_involutive (l : list A) : reverse (reverse l) = l.
 Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.
 
+(** ** Properties of the [take] function *)
 Lemma take_nil n :
   take n (@nil A) = [].
 Proof. by destruct n. Qed.
@@ -662,6 +763,7 @@ Lemma take_insert (l : list A) n i x :
   n â‰¤ i â†’ take n (<[i:=x]>l) = take n l.
 Proof take_alter _ _ _ _.
 
+(** ** Properties of the [drop] function *)
 Lemma drop_nil n :
   drop n (@nil A) = [].
 Proof. by destruct n. Qed.
@@ -698,6 +800,11 @@ Lemma drop_insert (l : list A) n i x :
   i < n â†’ drop n (<[i:=x]>l) = drop n l.
 Proof drop_alter _ _ _ _.
 
+Lemma delete_take_drop (l : list A) i :
+  delete i l = take i l ++ drop (S i) l.
+Proof. revert i. induction l; intros [|?]; simpl; auto using f_equal. Qed.
+
+(** ** Properties of the [replicate] function *)
 Lemma replicate_length n (x : A) : length (replicate n x) = n.
 Proof. induction n; simpl; auto. Qed.
 Lemma lookup_replicate n (x : A) i :
@@ -730,6 +837,7 @@ Lemma drop_replicate_plus n m (x : A) :
   drop n (replicate (n + m) x) = replicate m x.
 Proof. rewrite drop_replicate. f_equal. lia. Qed.
 
+(** ** Properties of the [resize] function *)
 Lemma resize_spec (l : list A) n x :
   resize n x l = take n l ++ replicate (n - length l) x.
 Proof.
@@ -863,10 +971,7 @@ Lemma drop_resize_plus (l : list A) n m x :
   drop n (resize (n + m) x l) = resize m x (drop n l).
 Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed.
 
-Lemma delete_take_drop (l : list A) i :
-  delete i l = take i l ++ drop (S i) l.
-Proof. revert i. induction l; intros [|?]; simpl; auto using f_equal. Qed.
-
+(** ** Properties of the [sublist] predicate *)
 Lemma sublist_nil_l (l : list A) :
   sublist [] l.
 Proof. induction l; try constructor; auto. Qed.
@@ -992,9 +1097,59 @@ Proof.
   * f_equal. auto with arith.
   * apply sublist_length in Hl12. lia.
 Qed.
+End general_properties.
+
+(** ** Properties of the [same_length] predicate *)
+Instance: âˆ€ A, Reflexive (@same_length A A).
+Proof. intros A l. induction l; constructor; auto. Qed.
+Instance: âˆ€ A, Symmetric (@same_length A A).
+Proof. induction 1; constructor; auto. Qed.
+
+Section same_length.
+  Context {A B : Type}.
+
+  Lemma same_length_length_1 (l : list A) (k : list B) :
+    same_length l k â†’ length l = length k.
+  Proof. induction 1; simpl; auto. Qed.
+  Lemma same_length_length_2 (l : list A) (k : list B) :
+    length l = length k â†’ same_length l k.
+  Proof.
+    revert k. induction l; intros [|??]; try discriminate;
+      constructor; auto with arith.
+  Qed.
+  Lemma same_length_length (l : list A) (k : list B) :
+    same_length l k â†” length l = length k.
+  Proof. split; auto using same_length_length_1, same_length_length_2. Qed.
+
+  Lemma same_length_lookup (l : list A) (k : list B) i :
+    same_length l k â†’ is_Some (l !! i) â†’ is_Some (k !! i).
+  Proof.
+    rewrite same_length_length.
+    setoid_rewrite lookup_lt_length.
+    intros E. by rewrite E.
+  Qed.
+
+  Lemma same_length_take (l1 : list A) (l2 : list B) n :
+    same_length l1 l2 â†’
+    same_length (take n l1) (take n l2).
+  Proof.
+    intros Hl. revert n; induction Hl; intros [|n]; constructor; auto.
+  Qed.
+  Lemma same_length_drop (l1 : list A) (l2 : list B) n :
+    same_length l1 l2 â†’
+    same_length (drop n l1) (drop n l2).
+  Proof.
+    intros Hl.
+    revert n; induction Hl; intros [|n]; simpl; try constructor; auto.
+  Qed.
+  Lemma same_length_resize (l1 : list A) (l2 : list B) x1 x2 n :
+    same_length (resize n x1 l1) (resize n x2 l2).
+  Proof. apply same_length_length. by rewrite !resize_length. Qed.
+End same_length.
 
+(** ** Properties of the [Forall] and [Exists] predicate *)
 Section Forall_Exists.
-  Context (P : A â†’ Prop).
+  Context {A} (P : A â†’ Prop).
 
   Lemma Forall_forall l :
     Forall P l â†” âˆ€ x, x âˆˆ l â†’ P x.
@@ -1043,13 +1198,16 @@ Section Forall_Exists.
   Lemma Forall_lookup l :
     Forall P l â†” âˆ€ i x, l !! i = Some x â†’ P x.
   Proof.
-    rewrite Forall_forall.
-    setoid_rewrite elem_of_list_lookup.
+    rewrite Forall_forall. setoid_rewrite elem_of_list_lookup.
     naive_solver.
   Qed.
   Lemma Forall_lookup_1 l i x :
     Forall P l â†’ l !! i = Some x â†’ P x.
   Proof. rewrite Forall_lookup. eauto. Qed.
+  Lemma Forall_lookup_2 l :
+    (âˆ€ i x, l !! i = Some x â†’ P x) â†’ Forall P l.
+  Proof. by rewrite Forall_lookup. Qed.
+
   Lemma Forall_alter f l i :
     Forall P l â†’
     (âˆ€ x, l !! i = Some x â†’ P x â†’ P (f x)) â†’
@@ -1135,8 +1293,8 @@ Section Forall_Exists.
     | right H => right (Forall_not_Exists _ H)
     end.
 End Forall_Exists.
-End general_properties.
 
+(** ** Properties of the [Forall2] predicate *)
 Section Forall2.
   Context {A B} (P : A â†’ B â†’ Prop).
 
@@ -1165,14 +1323,31 @@ Section Forall2.
     Forall2 P [] (x2 :: l2) â†’ False.
   Proof. by inversion 1. Qed.
 
-  Lemma Forall2_flip l1 l2 :
-    Forall2 P l1 l2 â†” Forall2 (flip P) l2 l1.
-  Proof. split; induction 1; constructor; auto. Qed.
+  Lemma Forall2_app_inv l1 l2 k1 k2 :
+    same_length l1 k1 â†’
+    Forall2 P (l1 ++ l2) (k1 ++ k2) â†’
+    Forall2 P l1 k1 âˆ§ Forall2 P l2 k2.
+  Proof. induction 1. done. inversion 1; naive_solver. Qed.
+  Lemma Forall2_app_inv_l l1 l2 k :
+    Forall2 P (l1 ++ l2) k â†’
+      âˆƒ k1 k2, Forall2 P l1 k1 âˆ§ Forall2 P l2 k2 âˆ§ k = k1 ++ k2.
+  Proof. revert k. induction l1; simpl; inversion 1; naive_solver. Qed.
+  Lemma Forall2_app_inv_r l k1 k2 :
+    Forall2 P l (k1 ++ k2) â†’
+      âˆƒ l1 l2, Forall2 P l1 k1 âˆ§ Forall2 P l2 k2 âˆ§ l = l1 ++ l2.
+  Proof. revert l. induction k1; simpl; inversion 1; naive_solver. Qed.
 
   Lemma Forall2_length l1 l2 :
     Forall2 P l1 l2 â†’ length l1 = length l2.
   Proof. induction 1; simpl; auto. Qed.
+  Lemma Forall2_same_length l1 l2 :
+    Forall2 P l1 l2 â†’
+    same_length l1 l2.
+  Proof. induction 1; constructor; auto. Qed.
 
+  Lemma Forall2_flip l1 l2 :
+    Forall2 P l1 l2 â†” Forall2 (flip P) l2 l1.
+  Proof. split; induction 1; constructor; auto. Qed.
   Lemma Forall2_impl (Q : A â†’ B â†’ Prop) l1 l2 :
     Forall2 P l1 l2 â†’ (âˆ€ x y, P x y â†’ Q x y) â†’ Forall2 Q l1 l2.
   Proof. intros H ?. induction H; auto. Defined.
@@ -1198,7 +1373,7 @@ Section Forall2.
     Forall Q k.
   Proof. induction 1; inversion_clear 1; eauto. Qed.
 
-  Lemma Forall2_lookup l1 l2 i x y :
+  Lemma Forall2_lookup_lr l1 l2 i x y :
     Forall2 P l1 l2 â†’
       l1 !! i = Some x â†’ l2 !! i = Some y â†’ P x y.
   Proof.
@@ -1223,6 +1398,25 @@ Section Forall2.
     * intros [|?] ?; simpl in *; simplify_equality; eauto.
   Qed.
 
+  Lemma Forall2_lookup_2 l1 l2 :
+    same_length l1 l2 â†’
+    (âˆ€ i x y, l1 !! i = Some x â†’ l2 !! i = Some y â†’ P x y) â†’
+    Forall2 P l1 l2.
+  Proof.
+    eauto using Forall2_same_length, Forall2_lookup_lr.
+    intros Hl Hlookup. induction Hl as [|????? IH]; constructor.
+    * by apply (Hlookup 0).
+    * apply IH. intros i. apply (Hlookup (S i)).
+  Qed.
+  Lemma Forall2_lookup l1 l2 :
+    Forall2 P l1 l2 â†” same_length l1 l2 âˆ§
+      (âˆ€ i x y, l1 !! i = Some x â†’ l2 !! i = Some y â†’ P x y).
+  Proof.
+    split.
+    * eauto using Forall2_same_length, Forall2_lookup_lr.
+    * intros [??]; eauto using Forall2_lookup_2.
+  Qed.
+
   Lemma Forall2_alter_l f l1 l2 i :
     Forall2 P l1 l2 â†’
     (âˆ€ x1 x2,
@@ -1362,780 +1556,643 @@ End Forall2.
 Section Forall2_order.
   Context  {A} (R : relation A).
 
+  Global Instance: Reflexive R â†’ Reflexive (Forall2 R).
+  Proof. intros ? l. induction l; by constructor. Qed.
+  Global Instance: Symmetric R â†’ Symmetric (Forall2 R).
+  Proof. intros. induction 1; constructor; auto. Qed.
+  Global Instance: Transitive R â†’ Transitive (Forall2 R).
+  Proof. intros ????. apply Forall2_trans. apply transitivity. Qed.
   Global Instance: PreOrder R â†’ PreOrder (Forall2 R).
-  Proof.
-    split.
-    * intros l. induction l; by constructor.
-    * intros ???. apply Forall2_trans. apply transitivity.
-  Qed.
+  Proof. split; apply _. Qed.
   Global Instance: AntiSymmetric R â†’ AntiSymmetric (Forall2 R).
   Proof. induction 2; inversion_clear 1; f_equal; auto. Qed.
 End Forall2_order.
 
-Ltac decompose_elem_of_list := repeat
-  match goal with
-  | H : ?x âˆˆ [] |- _ => by destruct (not_elem_of_nil x)
-  | H : _ âˆˆ _ :: _ |- _ => apply elem_of_cons in H; destruct H
-  | H : _ âˆˆ _ ++ _ |- _ => apply elem_of_app in H; destruct H
-  end.
-Ltac decompose_Forall := repeat
-  match goal with
-  | H : Forall _ [] |- _ => clear H
-  | H : Forall _ (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
-  | H : Forall _ (_ ++ _) |- _ => rewrite Forall_app in H; destruct H
-  | H : Forall2 _ [] [] |- _ => clear H
-  | H : Forall2 _ (_ :: _) [] |- _ => destruct (Forall2_cons_nil_inv _ _ _ H)
-  | H : Forall2 _ [] (_ :: _) |- _ => destruct (Forall2_nil_cons_inv _ _ _ H)
-  | H : Forall2 _ [] ?l |- _ => apply Forall2_nil_inv_l in H; subst l
-  | H : Forall2 _ ?l [] |- _ => apply Forall2_nil_inv_r in H; subst l
-  | H : Forall2 _ (_ :: _) (_ :: _) |- _ =>
-     apply Forall2_cons_inv in H; destruct H
-  | H : Forall2 _ (_ :: _) ?l |- _ =>
-     apply Forall2_cons_inv_l in H; destruct H as (? & ? & ? & ? & ?); subst l
-  | H : Forall2 _ ?l (_ :: _) |- _ =>
-     apply Forall2_cons_inv_r in H; destruct H as (? & ? & ? & ? & ?); subst l
-  end.
-
-(** * Theorems on the prefix and suffix predicates *)
-Section prefix_postfix.
-  Context {A : Type}.
+(** * Properties of the monadic operations *)
+Section fmap.
+  Context {A B : Type} (f : A â†’ B).
 
-  Global Instance: PreOrder (@prefix_of A).
-  Proof.
-    split.
-    * intros ?. eexists []. by rewrite (right_id [] (++)).
-    * intros ??? [k1 ?] [k2 ?].
-      exists (k1 ++ k2). subst. by rewrite (associative (++)).
-  Qed.
+  Lemma list_fmap_compose {C} (g : B â†’ C) l :
+    g âˆ˜ f <$> l = g <$> f <$> l.
+  Proof. induction l; simpl; f_equal; auto. Qed.
 
-  Lemma prefix_of_nil (l : list A) : prefix_of [] l.
-  Proof. by exists l. Qed.
-  Lemma prefix_of_nil_not x (l : list A) : Â¬prefix_of (x :: l) [].
-  Proof. by intros [k E]. Qed.
-  Lemma prefix_of_cons x (l1 l2 : list A) :
-    prefix_of l1 l2 â†’ prefix_of (x :: l1) (x :: l2).
-  Proof. intros [k E]. exists k. by subst. Qed.
-  Lemma prefix_of_cons_alt x y (l1 l2 : list A) :
-    x = y â†’ prefix_of l1 l2 â†’ prefix_of (x :: l1) (y :: l2).
-  Proof. intro. subst. apply prefix_of_cons. Qed.
-  Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) :
-    prefix_of (x :: l1) (y :: l2) â†’ x = y.
-  Proof. intros [k E]. by injection E. Qed.
-  Lemma prefix_of_cons_inv_2 x y (l1 l2 : list A) :
-    prefix_of (x :: l1) (y :: l2) â†’ prefix_of l1 l2.
-  Proof. intros [k E]. exists k. by injection E. Qed.
+  Lemma list_fmap_ext (g : A â†’ B) (l : list A) :
+    (âˆ€ x, f x = g x) â†’ fmap f l = fmap g l.
+  Proof. intro. induction l; simpl; f_equal; auto. Qed.
 
-  Lemma prefix_of_app k (l1 l2 : list A) :
-    prefix_of l1 l2 â†’ prefix_of (k ++ l1) (k ++ l2).
-  Proof. intros [k' ?]. subst. exists k'. by rewrite (associative (++)). Qed.
-  Lemma prefix_of_app_alt k1 k2 (l1 l2 : list A) :
-    k1 = k2 â†’ prefix_of l1 l2 â†’ prefix_of (k1 ++ l1) (k2 ++ l2).
-  Proof. intro. subst. apply prefix_of_app. Qed.
-  Lemma prefix_of_app_l (l1 l2 l3 : list A) :
-    prefix_of (l1 ++ l3) l2 â†’ prefix_of l1 l2.
+  Global Instance: Injective (=) (=) f â†’ Injective (=) (=) (fmap f).
   Proof.
-    intros [k ?]. red. exists (l3 ++ k). subst.
-    by rewrite <-(associative (++)).
+    intros ? l1. induction l1 as [|x l1 IH].
+    * by intros [|??].
+    * intros [|??]; simpl; intros; f_equal; simplify_equality; auto.
   Qed.
-  Lemma prefix_of_app_r (l1 l2 l3 : list A) :
-    prefix_of l1 l2 â†’ prefix_of l1 (l2 ++ l3).
+  Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
+  Proof. induction l1; simpl; by f_equal. Qed.
+
+  Lemma fmap_nil_inv k :
+    f <$> k = [] â†’ k = [].
+  Proof. by destruct k. Qed.
+  Lemma fmap_cons_inv y l k :
+    f <$> l = y :: k â†’
+    âˆƒ x l',
+      y = f x âˆ§
+      k = f <$> l' âˆ§
+      l = x :: l'.
+  Proof. intros. destruct l; simpl; simplify_equality; eauto. Qed.
+  Lemma fmap_app_inv l k1 k2 :
+    f <$> l = k1 ++ k2 â†’
+    âˆƒ l1 l2,
+      k1 = f <$> l1 âˆ§
+      k2 = f <$> l2 âˆ§
+      l = l1 ++ l2.
   Proof.
-    intros [k ?]. exists (k ++ l3). subst.
-    by rewrite (associative (++)).
+    revert l. induction k1 as [|y k1 IH]; simpl.
+    * intros l ?. by eexists [], l.
+    * intros [|x l] ?; simpl; simplify_equality.
+      destruct (IH l) as [l1 [l2 [? [??]]]]; subst; [done |].
+      by exists (x :: l1) l2.
   Qed.
 
-  Lemma prefix_of_length (l1 l2 : list A) :
-    prefix_of l1 l2 â†’ length l1 â‰¤ length l2.
-  Proof. intros [??]. subst. rewrite app_length. lia. Qed.
-  Lemma prefix_of_snoc_not (l : list A) x : Â¬prefix_of (l ++ [x]) l.
-  Proof. intros [??]. discriminate_list_equality. Qed.
-
-  Global Instance: PreOrder (@suffix_of A).
+  Lemma fmap_length l : length (f <$> l) = length l.
+  Proof. induction l; simpl; by f_equal. Qed.
+  Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
   Proof.
-    split.
-    * intros ?. by eexists [].
-    * intros ??? [k1 ?] [k2 ?].
-      exists (k2 ++ k1). subst. by rewrite (associative (++)).
+    induction l; simpl; [done |].
+    by rewrite !reverse_cons, fmap_app, IHl.
   Qed.
+  Lemma fmap_replicate n x :
+    f <$> replicate n x = replicate n (f x).
+  Proof. induction n; simpl; f_equal; auto. Qed.
 
-  Global Instance prefix_of_dec `{âˆ€ x y : A, Decision (x = y)} :
-      âˆ€ l1 l2 : list A, Decision (prefix_of l1 l2) :=
-    fix go l1 l2 :=
-    match l1, l2 return { prefix_of l1 l2 } + { Â¬prefix_of l1 l2 } with
-    | [], _ => left (prefix_of_nil _)
-    | _, [] => right (prefix_of_nil_not _ _)
-    | x :: l1, y :: l2 =>
-      match decide_rel (=) x y with
-      | left Exy =>
-        match go l1 l2 with
-        | left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Exy Hl1l2)
-        | right Hl1l2 => right (Hl1l2 âˆ˜ prefix_of_cons_inv_2 _ _ _ _)
-        end
-      | right Exy => right (Exy âˆ˜ prefix_of_cons_inv_1 _ _ _ _)
-      end
-    end.
-
-  Section prefix_ops.
-    Context `{âˆ€ x y : A, Decision (x = y)}.
-
-    Lemma max_prefix_of_fst (l1 l2 : list A) :
-      l1 = snd (max_prefix_of l1 l2) ++ fst (fst (max_prefix_of l1 l2)).
-    Proof.
-      revert l2. induction l1; intros [|??]; simpl;
-        repeat case_decide; simpl; f_equal; auto.
-    Qed.
-    Lemma max_prefix_of_fst_alt (l1 l2 : list A) k1 k2 k3 :
-      max_prefix_of l1 l2 = (k1,k2,k3) â†’ l1 = k3 ++ k1.
-    Proof.
-      intro. pose proof (max_prefix_of_fst l1 l2).
-      by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
-    Qed.
-    Lemma max_prefix_of_fst_prefix (l1 l2 : list A) :
-      prefix_of (snd (max_prefix_of l1 l2)) l1.
-    Proof. eexists. apply max_prefix_of_fst. Qed.
-    Lemma max_prefix_of_fst_prefix_alt (l1 l2 : list A) k1 k2 k3 :
-      max_prefix_of l1 l2 = (k1,k2,k3) â†’ prefix_of k3 l1.
-    Proof. eexists. eauto using max_prefix_of_fst_alt. Qed.
-
-    Lemma max_prefix_of_snd (l1 l2 : list A) :
-      l2 = snd (max_prefix_of l1 l2) ++ snd (fst (max_prefix_of l1 l2)).
-    Proof.
-      revert l2. induction l1; intros [|??]; simpl;
-        repeat case_decide; simpl; f_equal; auto.
-    Qed.
-    Lemma max_prefix_of_snd_alt (l1 l2 : list A) k1 k2 k3 :
-      max_prefix_of l1 l2 = (k1,k2,k3) â†’ l2 = k3 ++ k2.
-    Proof.
-      intro. pose proof (max_prefix_of_snd l1 l2).
-      by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
-    Qed.
-    Lemma max_prefix_of_snd_prefix (l1 l2 : list A) :
-      prefix_of (snd (max_prefix_of l1 l2)) l2.
-    Proof. eexists. apply max_prefix_of_snd. Qed.
-    Lemma max_prefix_of_snd_prefix_alt (l1 l2 : list A) k1 k2 k3 :
-      max_prefix_of l1 l2 = (k1,k2,k3) â†’ prefix_of k3 l2.
-    Proof. eexists. eauto using max_prefix_of_snd_alt. Qed.
-
-    Lemma max_prefix_of_max (l1 l2 : list A) k :
-      prefix_of k l1 â†’
-      prefix_of k l2 â†’
-      prefix_of k (snd (max_prefix_of l1 l2)).
-    Proof.
-      intros [l1' ?] [l2' ?]. subst.
-      by induction k; simpl; repeat case_decide; simpl;
-        auto using prefix_of_nil, prefix_of_cons.
-    Qed.
-    Lemma max_prefix_of_max_alt (l1 l2 : list A) k1 k2 k3 k :
-      max_prefix_of l1 l2 = (k1,k2,k3) â†’
-      prefix_of k l1 â†’
-      prefix_of k l2 â†’
-      prefix_of k k3.
-    Proof.
-      intro. pose proof (max_prefix_of_max l1 l2 k).
-      by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
-    Qed.
-
-    Lemma max_prefix_of_max_snoc (l1 l2 : list A) k1 k2 k3 x1 x2 :
-      max_prefix_of l1 l2 = (x1 :: k1, x2 :: k2, k3) â†’
-      x1 â‰  x2.
-    Proof.
-      intros Hl ?. subst. destruct (prefix_of_snoc_not k3 x2).
-      eapply max_prefix_of_max_alt; eauto.
-      * rewrite (max_prefix_of_fst_alt _ _ _ _ _ Hl).
-        apply prefix_of_app, prefix_of_cons, prefix_of_nil.
-      * rewrite (max_prefix_of_snd_alt _ _ _ _ _ Hl).
-        apply prefix_of_app, prefix_of_cons, prefix_of_nil.
-    Qed.
-  End prefix_ops.
-
-  Lemma prefix_suffix_reverse (l1 l2 : list A) :
-    prefix_of l1 l2 â†” suffix_of (reverse l1) (reverse l2).
+  Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
+  Proof. revert i. induction l; by intros [|]. Qed.
+  Lemma list_lookup_fmap_inv l i x :
+    (f <$> l) !! i = Some x â†’ âˆƒ y, x = f y âˆ§ l !! i = Some y.
   Proof.
-    split; intros [k E]; exists (reverse k).
-    * by rewrite E, reverse_app.
-    * by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
+    intros Hi. rewrite list_lookup_fmap in Hi.
+    destruct (l !! i) eqn:?; simplify_equality; eauto.
   Qed.
-  Lemma suffix_prefix_reverse (l1 l2 : list A) :
-    suffix_of l1 l2 â†” prefix_of (reverse l1) (reverse l2).
-  Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
-
-  Lemma suffix_of_nil (l : list A) : suffix_of [] l.
-  Proof. exists l. by rewrite (right_id [] (++)). Qed.
-  Lemma suffix_of_nil_inv (l : list A) : suffix_of l [] â†’ l = [].
-  Proof. by intros [[|?] ?]; simplify_list_equality. Qed.
-  Lemma suffix_of_cons_nil_inv x (l : list A) : Â¬suffix_of (x :: l) [].
-  Proof. by intros [[] ?]. Qed.
-  Lemma suffix_of_snoc (l1 l2 : list A) x :
-    suffix_of l1 l2 â†’ suffix_of (l1 ++ [x]) (l2 ++ [x]).
-  Proof. intros [k E]. exists k. subst. by rewrite (associative (++)). Qed.
-  Lemma suffix_of_snoc_alt x y (l1 l2 : list A) :
-    x = y â†’ suffix_of l1 l2 â†’ suffix_of (l1 ++ [x]) (l2 ++ [y]).
-  Proof. intro. subst. apply suffix_of_snoc. Qed.
-
-  Lemma suffix_of_app (l1 l2 k : list A) :
-    suffix_of l1 l2 â†’ suffix_of (l1 ++ k) (l2 ++ k).
-  Proof. intros [k' E]. exists k'. subst. by rewrite (associative (++)). Qed.
-  Lemma suffix_of_app_alt (l1 l2 k1 k2 : list A) :
-    k1 = k2 â†’ suffix_of l1 l2 â†’ suffix_of (l1 ++ k1) (l2 ++ k2).
-  Proof. intro. subst. apply suffix_of_app. Qed.
 
-  Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) :
-    suffix_of (l1 ++ [x]) (l2 ++ [y]) â†’ x = y.
+  Lemma list_alter_fmap (g : A â†’ A) (h : B â†’ B) l i :
+    Forall (Î» x, f (g x) = h (f x)) l â†’
+    f <$> alter g i l = alter h i (f <$> l).
   Proof.
-    rewrite suffix_prefix_reverse, !reverse_snoc.
-    by apply prefix_of_cons_inv_1.
+    intros Hl. revert i.
+    induction Hl; intros [|i]; simpl; f_equal; auto.
   Qed.
-  Lemma suffix_of_snoc_inv_2 x y (l1 l2 : list A) :
-    suffix_of (l1 ++ [x]) (l2 ++ [y]) â†’ suffix_of l1 l2.
+  Lemma elem_of_list_fmap_1 l x : x âˆˆ l â†’ f x âˆˆ f <$> l.
+  Proof. induction 1; simpl; rewrite elem_of_cons; intuition. Qed.
+  Lemma elem_of_list_fmap_1_alt l x y : x âˆˆ l â†’ y = f x â†’ y âˆˆ f <$> l.
+  Proof. intros. subst. by apply elem_of_list_fmap_1. Qed.
+  Lemma elem_of_list_fmap_2 l x : x âˆˆ f <$> l â†’ âˆƒ y, x = f y âˆ§ y âˆˆ l.
   Proof.
-    rewrite !suffix_prefix_reverse, !reverse_snoc.
-    by apply prefix_of_cons_inv_2.
+    induction l as [|y l IH]; simpl; inversion_clear 1.
+    + exists y. split; [done | by left].
+    + destruct IH as [z [??]]. done. exists z. split; [done | by right].
   Qed.
-
-  Lemma suffix_of_cons_l (l1 l2 : list A) x :
-    suffix_of (x :: l1) l2 â†’ suffix_of l1 l2.
+  Lemma elem_of_list_fmap l x : x âˆˆ f <$> l â†” âˆƒ y, x = f y âˆ§ y âˆˆ  l.
   Proof.
-    intros [k ?]. exists (k ++ [x]). subst.
-    by rewrite <-(associative (++)).
+    firstorder eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
   Qed.
-  Lemma suffix_of_app_l (l1 l2 l3 : list A) :
-    suffix_of (l3 ++ l1) l2 â†’ suffix_of l1 l2.
+
+  Lemma NoDup_fmap_1 (l : list A) :
+    NoDup (f <$> l) â†’ NoDup l.
   Proof.
-    intros [k ?]. exists (k ++ l3). subst.
-    by rewrite <-(associative (++)).
+    induction l; simpl; inversion_clear 1; constructor; auto.
+    rewrite elem_of_list_fmap in *. naive_solver.
   Qed.
-  Lemma suffix_of_cons_r (l1 l2 : list A) x :
-    suffix_of l1 l2 â†’ suffix_of l1 (x :: l2).
-  Proof. intros [k ?]. exists (x :: k). by subst. Qed.
-  Lemma suffix_of_app_r (l1 l2 l3 : list A) :
-    suffix_of l1 l2 â†’ suffix_of l1 (l3 ++ l2).
+  Lemma NoDup_fmap_2 `{!Injective (=) (=) f} (l : list A) :
+    NoDup l â†’ NoDup (f <$> l).
   Proof.
-    intros [k ?]. exists (l3 ++ k). subst.
-    by rewrite (associative (++)).
+    induction 1; simpl; constructor; trivial.
+    rewrite elem_of_list_fmap. intros [y [Hxy ?]].
+    apply (injective f) in Hxy. by subst.
   Qed.
+  Lemma NoDup_fmap `{!Injective (=) (=) f} (l : list A) :
+    NoDup (f <$> l) â†” NoDup l.
+  Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
 
-  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.
+  Global Instance fmap_Permutation_proper:
+    Proper (Permutation ==> Permutation) (fmap f).
+  Proof. induction 1; simpl; econstructor; eauto. Qed.
+
+  Lemma Forall_fmap_ext (g : A â†’ B) (l : list A) :
+    Forall (Î» x, f x = g x) l â†” fmap f l = fmap g l.
   Proof.
-    intros [[|? k] E].
-    * by left.
-    * right. simplify_equality. by apply suffix_of_app_r.
+    split.
+    * induction 1; simpl; f_equal; auto.
+    * induction l; simpl; constructor; simplify_equality; auto.
+  Qed.
+  Lemma Forall_fmap (l : list A) (P : B â†’ Prop) :
+    Forall P (f <$> l) â†” Forall (P âˆ˜ f) l.
+  Proof.
+    split; induction l; inversion_clear 1; constructor; auto.
   Qed.
 
-  Lemma suffix_of_length (l1 l2 : list A) :
-    suffix_of l1 l2 â†’ length l1 â‰¤ length l2.
-  Proof. intros [??]. subst. rewrite app_length. lia. Qed.
-  Lemma suffix_of_cons_not x (l : list A) : Â¬suffix_of (x :: l) l.
-  Proof. intros [??]. discriminate_list_equality. Qed.
+  Lemma Forall2_fmap_l {C} (P : B â†’ C â†’ Prop) l1 l2 :
+    Forall2 P (f <$> l1) l2 â†” Forall2 (P âˆ˜ f) l1 l2.
+  Proof.
+    split; revert l2; induction l1; inversion_clear 1; constructor; auto.
+  Qed.
+  Lemma Forall2_fmap_r {C} (P : C â†’ B â†’ Prop) l1 l2 :
+    Forall2 P l1 (f <$> l2) â†” Forall2 (Î» x, P x âˆ˜ f) l1 l2.
+  Proof.
+    split; revert l1; induction l2; inversion_clear 1; constructor; auto.
+  Qed.
+  Lemma Forall2_fmap_1 {C D} (g : C â†’ D) (P : B â†’ D â†’ Prop) l1 l2 :
+    Forall2 P (f <$> l1) (g <$> l2) â†’
+    Forall2 (Î» x1 x2, P (f x1) (g x2)) l1 l2.
+  Proof. revert l2; induction l1; intros [|??]; inversion_clear 1; auto. Qed.
+  Lemma Forall2_fmap_2 {C D} (g : C â†’ D) (P : B â†’ D â†’ Prop) l1 l2 :
+    Forall2 (Î» x1 x2, P (f x1) (g x2)) l1 l2 â†’
+    Forall2 P (f <$> l1) (g <$> l2).
+  Proof. induction 1; simpl; auto. Qed.
+  Lemma Forall2_fmap {C D} (g : C â†’ D) (P : B â†’ D â†’ Prop) l1 l2 :
+    Forall2 P (f <$> l1) (g <$> l2) â†”
+    Forall2 (Î» x1 x2, P (f x1) (g x2)) l1 l2.
+  Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.
 
-  Global Instance suffix_of_dec `{âˆ€ x y : A, Decision (x = y)}
-    (l1 l2 : list A) : Decision (suffix_of l1 l2).
+  Lemma mapM_fmap_Some (g : B â†’ option A) (l : list A) :
+    (âˆ€ x, g (f x) = Some x) â†’
+    mapM g (f <$> l) = Some l.
+  Proof. intros. by induction l; simpl; simplify_option_equality. Qed.
+  Lemma mapM_fmap_Some_inv (g : B â†’ option A) (l : list A) (k : list B) :
+    (âˆ€ x y, g y = Some x â†’ y = f x) â†’
+    mapM g k = Some l â†’
+    k = f <$> l.
   Proof.
-    refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
-     abstract (by rewrite suffix_prefix_reverse).
-  Defined.
+    intros Hgf. revert l; induction k as [|??]; intros [|??] ?;
+      simplify_option_equality; f_equiv; eauto.
+  Qed.
+End fmap.
 
-  Section max_suffix_of.
-    Context `{âˆ€ x y : A, Decision (x = y)}.
+Lemma NoDup_fmap_fst {A B} (l : list (A * B)) :
+  (âˆ€ x y1 y2, (x,y1) âˆˆ l â†’ (x,y2) âˆˆ l â†’ y1 = y2) â†’
+  NoDup l â†’
+  NoDup (fst <$> l).
+Proof.
+  intros Hunique.
+  induction 1 as [|[x1 y1] l Hin Hnodup IH]; simpl; constructor.
+  * rewrite elem_of_list_fmap.
+    intros [[x2 y2] [??]]; simpl in *; subst. destruct Hin.
+    rewrite (Hunique x2 y1 y2); rewrite ?elem_of_cons; auto.
+  * apply IH. intros.
+    eapply Hunique; rewrite ?elem_of_cons; eauto.
+Qed.
 
-    Lemma max_suffix_of_fst (l1 l2 : list A) :
-      l1 = fst (fst (max_suffix_of l1 l2)) ++ snd (max_suffix_of l1 l2).
-    Proof.
-      rewrite <-(reverse_involutive l1) at 1.
-      rewrite (max_prefix_of_fst (reverse l1) (reverse l2)).
-      unfold max_suffix_of.
-      destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
-      by rewrite reverse_app.
-    Qed.
-    Lemma max_suffix_of_fst_alt (l1 l2 : list A) k1 k2 k3 :
-      max_suffix_of l1 l2 = (k1,k2,k3) â†’ l1 = k1 ++ k3.
-    Proof.
-      intro. pose proof (max_suffix_of_fst l1 l2).
-      by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
-    Qed.
-    Lemma max_suffix_of_fst_suffix (l1 l2 : list A) :
-      suffix_of (snd (max_suffix_of l1 l2)) l1.
-    Proof. eexists. apply max_suffix_of_fst. Qed.
-    Lemma max_suffix_of_fst_suffix_alt (l1 l2 : list A) k1 k2 k3 :
-      max_suffix_of l1 l2 = (k1,k2,k3) â†’ suffix_of k3 l1.
-    Proof. eexists. eauto using max_suffix_of_fst_alt. Qed.
-
-    Lemma max_suffix_of_snd (l1 l2 : list A) :
-      l2 = snd (fst (max_suffix_of l1 l2)) ++ snd (max_suffix_of l1 l2).
-    Proof.
-      rewrite <-(reverse_involutive l2) at 1.
-      rewrite (max_prefix_of_snd (reverse l1) (reverse l2)).
-      unfold max_suffix_of.
-      destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
-      by rewrite reverse_app.
-    Qed.
-    Lemma max_suffix_of_snd_alt (l1 l2 : list A) k1 k2 k3 :
-      max_suffix_of l1 l2 = (k1,k2,k3) â†’ l2 = k2 ++ k3.
-    Proof.
-      intro. pose proof (max_suffix_of_snd l1 l2).
-      by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
-    Qed.
-    Lemma max_suffix_of_snd_suffix (l1 l2 : list A) :
-      suffix_of (snd (max_suffix_of l1 l2)) l2.
-    Proof. eexists. apply max_suffix_of_snd. Qed.
-    Lemma max_suffix_of_snd_suffix_alt (l1 l2 : list A) k1 k2 k3 :
-      max_suffix_of l1 l2 = (k1,k2,k3) â†’ suffix_of k3 l2.
-    Proof. eexists. eauto using max_suffix_of_snd_alt. Qed.
-
-    Lemma max_suffix_of_max (l1 l2 : list A) k :
-      suffix_of k l1 â†’
-      suffix_of k l2 â†’
-      suffix_of k (snd (max_suffix_of l1 l2)).
-    Proof.
-      generalize (max_prefix_of_max (reverse l1) (reverse l2)).
-      rewrite !suffix_prefix_reverse. unfold max_suffix_of.
-      destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
-      rewrite reverse_involutive. auto.
-    Qed.
-    Lemma max_suffix_of_max_alt (l1 l2 : list A) k1 k2 k3 k :
-      max_suffix_of l1 l2 = (k1,k2,k3) â†’
-      suffix_of k l1 â†’
-      suffix_of k l2 â†’
-      suffix_of k k3.
-    Proof.
-      intro. pose proof (max_suffix_of_max l1 l2 k).
-      by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
-    Qed.
-
-    Lemma max_suffix_of_max_snoc (l1 l2 : list A) k1 k2 k3 x1 x2 :
-      max_suffix_of l1 l2 = (k1 ++ [x1], k2 ++ [x2], k3) â†’
-      x1 â‰  x2.
-    Proof.
-      intros Hl ?. subst. destruct (suffix_of_cons_not x2 k3).
-      eapply max_suffix_of_max_alt; eauto.
-      * rewrite (max_suffix_of_fst_alt _ _ _ _ _ Hl).
-        by apply (suffix_of_app [x2]), suffix_of_app_r.
-      * rewrite (max_suffix_of_snd_alt _ _ _ _ _ Hl).
-        by apply (suffix_of_app [x2]), suffix_of_app_r.
-    Qed.
-  End max_suffix_of.
-End prefix_postfix.
-
-(** The [simplify_suffix_of] tactic removes [suffix_of] hypotheses that are
-tautologies, and simplifies [suffix_of] hypotheses involving [(::)] and
-[(++)]. *)
-Ltac simplify_suffix_of := repeat
-  match goal with
-  | H : suffix_of (_ :: _) _ |- _ =>
-    destruct (suffix_of_cons_not _ _ H)
-  | H : suffix_of (_ :: _) [] |- _ =>
-    apply suffix_of_nil_inv in 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_equality
-  end.
-
-(** The [solve_suffix_of] tactic tries to solve goals involving [suffix_of]. It
-uses [simplify_suffix_of] to simplify hypotheses and tries to solve [suffix_of]
-conclusions. This tactic either fails or proves the goal. *)
-Ltac solve_suffix_of := solve [intuition (repeat
-  match goal with
-  | _ => done
-  | _ => progress simplify_suffix_of
-  | |- suffix_of [] _ => apply suffix_of_nil
-  | |- suffix_of _ _ => reflexivity
-  | |- suffix_of _ (_ :: _) => apply suffix_of_cons_r
-  | |- suffix_of _ (_ ++ _) => apply suffix_of_app_r
-  | H : suffix_of _ _ â†’ False |- _ => destruct H
-  end)].
-Hint Extern 0 (PropHolds (suffix_of _ _)) =>
-  unfold PropHolds; solve_suffix_of : typeclass_instances.
-
-(** * Folding lists *)
-Notation foldr := fold_right.
-Notation foldr_app := fold_right_app.
-
-Lemma foldr_permutation {A B} (R : relation B)
-   `{!Equivalence R}
-   (f : A â†’ B â†’ B) (b : B)
-   `{!Proper ((=) ==> R ==> R) f}
-   (Hf : âˆ€ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
-  Proper (Permutation ==> R) (foldr f b).
-Proof.
-  induction 1; simpl.
-  * done.
-  * by f_equiv.
-  * apply Hf.
-  * etransitivity; eauto.
-Qed.
-
-(** We redefine [foldl] with the arguments in the same order as in Haskell. *)
-Definition foldl {A B} (f : A â†’ B â†’ A) : A â†’ list B â†’ A :=
-  fix go a l :=
-  match l with
-  | [] => a
-  | x :: l => go (f a x) l
-  end.
+Section bind.
+  Context {A B : Type} (f : A â†’ list B).
 
-Lemma foldl_app {A B} (f : A â†’ B â†’ A) (l k : list B) (a : A) :
-  foldl f a (l ++ k) = foldl f (foldl f a l) k.
-Proof. revert a. induction l; simpl; auto. Qed.
+  Lemma bind_app (l1 l2 : list A) :
+    (l1 ++ l2) â‰«= f = (l1 â‰«= f) ++ (l2 â‰«= f).
+  Proof.
+    induction l1; simpl; [done|].
+    by rewrite <-(associative (++)), IHl1.
+  Qed.
+  Lemma elem_of_list_bind (x : B) (l : list A) :
+    x âˆˆ l â‰«= f â†” âˆƒ y, x âˆˆ f y âˆ§ y âˆˆ l.
+  Proof.
+    split.
+    * induction l as [|y l IH]; simpl.
+      { inversion 1. }
+      rewrite elem_of_app. intros [?|?].
+      + exists y. split; [done | by left].
+      + destruct IH as [z [??]]. done.
+        exists z. split; [done | by right].
+    * intros [y [Hx Hy]].
+      induction Hy; simpl; rewrite elem_of_app; intuition.
+  Qed.
 
-(** * Monadic operations *)
-Instance list_ret: MRet list := Î» A x, x :: @nil A.
-Instance list_fmap {A B} (f : A â†’ B) : FMapD list f :=
-  fix go (l : list A) :=
-  match l with
-  | [] => []
-  | x :: l => f x :: @fmap _ _ _ f go l
-  end.
-Instance list_bind {A B} (f : A â†’ list B) : MBindD list f :=
-  fix go (l : list A) :=
-  match l with
-  | [] => []
-  | x :: l => f x ++ @mbind _ _ _ f go l
-  end.
-Instance list_join: MJoin list :=
-  fix go A (ls : list (list A)) : list A :=
-  match ls with
-  | [] => []
-  | l :: ls => l ++ @mjoin _ go _ ls
-  end.
+  Lemma Forall2_bind {C D} (g : C â†’ list D) (P : B â†’ D â†’ Prop) l1 l2 :
+    Forall2 (Î» x1 x2, Forall2 P (f x1) (g x2)) l1 l2 â†’
+    Forall2 P (l1 â‰«= f) (l2 â‰«= g).
+  Proof. induction 1; simpl; auto using Forall2_app. Qed.
+End bind.
 
-Definition mapM `{!MBind M} `{!MRet M} {A B}
-    (f : A â†’ M B) : list A â†’ M (list B) :=
-  fix go l :=
-  match l with
-  | [] => mret []
-  | x :: l => y â† f x; k â† go l; mret (y :: k)
-  end.
+Section ret_join.
+  Context {A : Type}.
 
-Section list_fmap.
-  Context {A B : Type} (f : A â†’ B).
+  Lemma list_join_bind (ls : list (list A)) :
+    mjoin ls = ls â‰«= id.
+  Proof. induction ls; simpl; f_equal; auto. Qed.
 
-  Lemma list_fmap_compose {C} (g : B â†’ C) l :
-    g âˆ˜ f <$> l = g <$> f <$> l.
-  Proof. induction l; simpl; f_equal; auto. Qed.
+  Lemma elem_of_list_ret (x y : A) :
+    x âˆˆ @mret list _ A y â†” x = y.
+  Proof. apply elem_of_list_singleton. Qed.
+  Lemma elem_of_list_join (x : A) (ls : list (list A)) :
+    x âˆˆ mjoin ls â†” âˆƒ l, x âˆˆ l âˆ§ l âˆˆ ls.
+  Proof. by rewrite list_join_bind, elem_of_list_bind. Qed.
 
-  Lemma list_fmap_ext (g : A â†’ B) (l : list A) :
-    (âˆ€ x, f x = g x) â†’ fmap f l = fmap g l.
-  Proof. intro. induction l; simpl; f_equal; auto. Qed.
-  Lemma list_fmap_ext_alt (g : A â†’ B) (l : list A) :
-    Forall (Î» x, f x = g x) l â†” fmap f l = fmap g l.
+  Lemma join_nil (ls : list (list A)) :
+    mjoin ls = [] â†” Forall (= []) ls.
   Proof.
     split.
-    * induction 1; simpl; f_equal; auto.
-    * induction l; simpl; constructor; simplify_equality; auto.
+    * by induction ls as [|[|??] ?]; constructor; auto.
+    * by induction 1 as [|[|??] ?].
   Qed.
+  Lemma join_nil_1 (ls : list (list A)) :
+    mjoin ls = [] â†’ Forall (= []) ls.
+  Proof. by rewrite join_nil. Qed.
+  Lemma join_nil_2 (ls : list (list A)) :
+    Forall (= []) ls â†’ mjoin ls = [].
+  Proof. by rewrite join_nil. Qed.
 
-  Global Instance: Injective (=) (=) f â†’ Injective (=) (=) (fmap f).
-  Proof.
-    intros ? l1. induction l1 as [|x l1 IH].
-    * by intros [|??].
-    * intros [|??]; simpl; intros; f_equal; simplify_equality; auto.
-  Qed.
-  Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
-  Proof. induction l1; simpl; by f_equal. Qed.
+  Lemma join_length (ls : list (list A)) :
+    length (mjoin ls) = foldr (plus âˆ˜ length) 0 ls.
+  Proof. by induction ls; simpl; rewrite ?app_length; f_equal. Qed.
+  Lemma join_length_same (ls : list (list A)) n :
+    Forall (Î» l, length l = n) ls â†’
+    length (mjoin ls) = length ls * n.
+  Proof. rewrite join_length. by induction 1; simpl; f_equal. Qed.
 
-  Lemma fmap_nil_inv k :
-    f <$> k = [] â†’ k = [].
-  Proof. by destruct k. Qed.
-  Lemma fmap_cons_inv y l k :
-    f <$> l = y :: k â†’
-    âˆƒ x l',
-      y = f x âˆ§
-      k = f <$> l' âˆ§
-      l = x :: l'.
-  Proof. intros. destruct l; simpl; simplify_equality; eauto. Qed.
-  Lemma fmap_app_inv l k1 k2 :
-    f <$> l = k1 ++ k2 â†’
-    âˆƒ l1 l2,
-      k1 = f <$> l1 âˆ§
-      k2 = f <$> l2 âˆ§
-      l = l1 ++ l2.
+  Lemma lookup_join_same_length (ls : list (list A)) n i :
+    n â‰  0 â†’
+    Forall (Î» l, length l = n) ls â†’
+    mjoin ls !! i = ls !! (i `div` n) â‰«= (!! (i `mod` n)).
   Proof.
-    revert l. induction k1 as [|y k1 IH]; simpl.
-    * intros l ?. by eexists [], l.
-    * intros [|x l] ?; simpl; simplify_equality.
-      destruct (IH l) as [l1 [l2 [? [??]]]]; subst; [done |].
-      by exists (x :: l1) l2.
+    intros Hn Hls. revert i.
+    induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
+    destruct (decide (i < n)) as [Hin|Hin].
+    * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
+      rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
+      simpl. rewrite lookup_app_l; auto with lia.
+    * replace i with ((i - n) + 1 * n) by lia.
+      rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
+      replace (i - n + 1 * n) with i by lia.
+      rewrite (plus_comm _ 1), lookup_app_r_alt, IH by lia.
+      by subst.
   Qed.
 
-  Lemma fmap_length l : length (f <$> l) = length l.
-  Proof. induction l; simpl; by f_equal. Qed.
-  Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
+  (* This should be provable using the previous lemma in a shorter way *)
+  Lemma alter_join_same_length f (ls : list (list A)) n i :
+    n â‰  0 â†’
+    Forall (Î» l, length l = n) ls â†’
+    alter f i (mjoin ls) = mjoin (alter (alter f (i `mod` n)) (i `div` n) ls).
   Proof.
-    induction l; simpl; [done |].
-    by rewrite !reverse_cons, fmap_app, IHl.
+    intros Hn Hls. revert i.
+    induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
+    destruct (decide (i < n)) as [Hin|Hin].
+    * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
+      rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
+      simpl. rewrite alter_app_l; auto with lia.
+    * replace i with ((i - n) + 1 * n) by lia.
+      rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
+      replace (i - n + 1 * n) with i by lia.
+      rewrite (plus_comm _ 1), alter_app_r_alt, IH by lia.
+      by subst.
   Qed.
-  Lemma fmap_replicate n x :
-    f <$> replicate n x = replicate n (f x).
-  Proof. induction n; simpl; f_equal; auto. Qed.
+  Lemma insert_join_same_length (ls : list (list A)) n i x :
+    n â‰  0 â†’
+    Forall (Î» l, length l = n) ls â†’
+    <[i:=x]>(mjoin ls) = mjoin (alter <[i `mod` n:=x]> (i `div` n) ls).
+  Proof. apply alter_join_same_length. Qed.
 
-  Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
-  Proof. revert i. induction l; by intros [|]. Qed.
-  Lemma list_lookup_fmap_inv l i x :
-    (f <$> l) !! i = Some x â†’ âˆƒ y, x = f y âˆ§ l !! i = Some y.
+  Lemma Forall2_join {B} (P : A â†’ B â†’ Prop) ls1 ls2 :
+    Forall2 (Forall2 P) ls1 ls2 â†’
+    Forall2 P (mjoin ls1) (mjoin ls2).
+  Proof. induction 1; simpl; auto using Forall2_app. Qed.
+End ret_join.
+
+(** ** Properties of the [prefix_of] and [suffix_of] predicates *)
+Section prefix_postfix.
+  Context {A : Type}.
+
+  Global Instance: PreOrder (@prefix_of A).
   Proof.
-    intros Hi. rewrite list_lookup_fmap in Hi.
-    destruct (l !! i) eqn:?; simplify_equality; eauto.
+    split.
+    * intros ?. eexists []. by rewrite (right_id [] (++)).
+    * intros ??? [k1 ?] [k2 ?].
+      exists (k1 ++ k2). subst. by rewrite (associative (++)).
   Qed.
 
-  Lemma list_alter_fmap (g : A â†’ A) (h : B â†’ B) l i :
-    Forall (Î» x, f (g x) = h (f x)) l â†’
-    f <$> alter g i l = alter h i (f <$> l).
+  Lemma prefix_of_nil (l : list A) : prefix_of [] l.
+  Proof. by exists l. Qed.
+  Lemma prefix_of_nil_not x (l : list A) : Â¬prefix_of (x :: l) [].
+  Proof. by intros [k E]. Qed.
+  Lemma prefix_of_cons x (l1 l2 : list A) :
+    prefix_of l1 l2 â†’ prefix_of (x :: l1) (x :: l2).
+  Proof. intros [k E]. exists k. by subst. Qed.
+  Lemma prefix_of_cons_alt x y (l1 l2 : list A) :
+    x = y â†’ prefix_of l1 l2 â†’ prefix_of (x :: l1) (y :: l2).
+  Proof. intro. subst. apply prefix_of_cons. Qed.
+  Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) :
+    prefix_of (x :: l1) (y :: l2) â†’ x = y.
+  Proof. intros [k E]. by injection E. Qed.
+  Lemma prefix_of_cons_inv_2 x y (l1 l2 : list A) :
+    prefix_of (x :: l1) (y :: l2) â†’ prefix_of l1 l2.
+  Proof. intros [k E]. exists k. by injection E. Qed.
+
+  Lemma prefix_of_app k (l1 l2 : list A) :
+    prefix_of l1 l2 â†’ prefix_of (k ++ l1) (k ++ l2).
+  Proof. intros [k' ?]. subst. exists k'. by rewrite (associative (++)). Qed.
+  Lemma prefix_of_app_alt k1 k2 (l1 l2 : list A) :
+    k1 = k2 â†’ prefix_of l1 l2 â†’ prefix_of (k1 ++ l1) (k2 ++ l2).
+  Proof. intro. subst. apply prefix_of_app. Qed.
+  Lemma prefix_of_app_l (l1 l2 l3 : list A) :
+    prefix_of (l1 ++ l3) l2 â†’ prefix_of l1 l2.
   Proof.
-    intros Hl. revert i.
-    induction Hl; intros [|i]; simpl; f_equal; auto.
+    intros [k ?]. red. exists (l3 ++ k). subst.
+    by rewrite <-(associative (++)).
   Qed.
-  Lemma elem_of_list_fmap_1 l x : x âˆˆ l â†’ f x âˆˆ f <$> l.
-  Proof. induction 1; simpl; rewrite elem_of_cons; intuition. Qed.
-  Lemma elem_of_list_fmap_1_alt l x y : x âˆˆ l â†’ y = f x â†’ y âˆˆ f <$> l.
-  Proof. intros. subst. by apply elem_of_list_fmap_1. Qed.
-  Lemma elem_of_list_fmap_2 l x : x âˆˆ f <$> l â†’ âˆƒ y, x = f y âˆ§ y âˆˆ l.
+  Lemma prefix_of_app_r (l1 l2 l3 : list A) :
+    prefix_of l1 l2 â†’ prefix_of l1 (l2 ++ l3).
   Proof.
-    induction l as [|y l IH]; simpl; intros; decompose_elem_of_list.
-    + exists y. split; [done | by left].
-    + destruct IH as [z [??]]. done. exists z. split; [done | by right].
+    intros [k ?]. exists (k ++ l3). subst.
+    by rewrite (associative (++)).
   Qed.
-  Lemma elem_of_list_fmap l x : x âˆˆ f <$> l â†” âˆƒ y, x = f y âˆ§ y âˆˆ  l.
+
+  Lemma prefix_of_length (l1 l2 : list A) :
+    prefix_of l1 l2 â†’ length l1 â‰¤ length l2.
+  Proof. intros [??]. subst. rewrite app_length. lia. Qed.
+  Lemma prefix_of_snoc_not (l : list A) x : Â¬prefix_of (l ++ [x]) l.
+  Proof. intros [??]. discriminate_list_equality. Qed.
+
+  Global Instance: PreOrder (@suffix_of A).
   Proof.
-    firstorder eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
+    split.
+    * intros ?. by eexists [].
+    * intros ??? [k1 ?] [k2 ?].
+      exists (k2 ++ k1). subst. by rewrite (associative (++)).
   Qed.
 
-  Lemma NoDup_fmap_1 (l : list A) :
-    NoDup (f <$> l) â†’ NoDup l.
-  Proof.
-    induction l; simpl; inversion_clear 1; constructor; auto.
-    rewrite elem_of_list_fmap in *. naive_solver.
-  Qed.
-  Lemma NoDup_fmap_2 `{!Injective (=) (=) f} (l : list A) :
-    NoDup l â†’ NoDup (f <$> l).
+  Global Instance prefix_of_dec `{âˆ€ x y : A, Decision (x = y)} :
+      âˆ€ l1 l2 : list A, Decision (prefix_of l1 l2) :=
+    fix go l1 l2 :=
+    match l1, l2 return { prefix_of l1 l2 } + { Â¬prefix_of l1 l2 } with
+    | [], _ => left (prefix_of_nil _)
+    | _, [] => right (prefix_of_nil_not _ _)
+    | x :: l1, y :: l2 =>
+      match decide_rel (=) x y with
+      | left Exy =>
+        match go l1 l2 with
+        | left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Exy Hl1l2)
+        | right Hl1l2 => right (Hl1l2 âˆ˜ prefix_of_cons_inv_2 _ _ _ _)
+        end
+      | right Exy => right (Exy âˆ˜ prefix_of_cons_inv_1 _ _ _ _)
+      end
+    end.
+
+  Section prefix_ops.
+    Context `{âˆ€ x y : A, Decision (x = y)}.
+
+    Lemma max_prefix_of_fst (l1 l2 : list A) :
+      l1 = snd (max_prefix_of l1 l2) ++ fst (fst (max_prefix_of l1 l2)).
+    Proof.
+      revert l2. induction l1; intros [|??]; simpl;
+        repeat case_decide; simpl; f_equal; auto.
+    Qed.
+    Lemma max_prefix_of_fst_alt (l1 l2 : list A) k1 k2 k3 :
+      max_prefix_of l1 l2 = (k1,k2,k3) â†’ l1 = k3 ++ k1.
+    Proof.
+      intro. pose proof (max_prefix_of_fst l1 l2).
+      by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
+    Qed.
+    Lemma max_prefix_of_fst_prefix (l1 l2 : list A) :
+      prefix_of (snd (max_prefix_of l1 l2)) l1.
+    Proof. eexists. apply max_prefix_of_fst. Qed.
+    Lemma max_prefix_of_fst_prefix_alt (l1 l2 : list A) k1 k2 k3 :
+      max_prefix_of l1 l2 = (k1,k2,k3) â†’ prefix_of k3 l1.
+    Proof. eexists. eauto using max_prefix_of_fst_alt. Qed.
+
+    Lemma max_prefix_of_snd (l1 l2 : list A) :
+      l2 = snd (max_prefix_of l1 l2) ++ snd (fst (max_prefix_of l1 l2)).
+    Proof.
+      revert l2. induction l1; intros [|??]; simpl;
+        repeat case_decide; simpl; f_equal; auto.
+    Qed.
+    Lemma max_prefix_of_snd_alt (l1 l2 : list A) k1 k2 k3 :
+      max_prefix_of l1 l2 = (k1,k2,k3) â†’ l2 = k3 ++ k2.
+    Proof.
+      intro. pose proof (max_prefix_of_snd l1 l2).
+      by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
+    Qed.
+    Lemma max_prefix_of_snd_prefix (l1 l2 : list A) :
+      prefix_of (snd (max_prefix_of l1 l2)) l2.
+    Proof. eexists. apply max_prefix_of_snd. Qed.
+    Lemma max_prefix_of_snd_prefix_alt (l1 l2 : list A) k1 k2 k3 :
+      max_prefix_of l1 l2 = (k1,k2,k3) â†’ prefix_of k3 l2.
+    Proof. eexists. eauto using max_prefix_of_snd_alt. Qed.
+
+    Lemma max_prefix_of_max (l1 l2 : list A) k :
+      prefix_of k l1 â†’
+      prefix_of k l2 â†’
+      prefix_of k (snd (max_prefix_of l1 l2)).
+    Proof.
+      intros [l1' ?] [l2' ?]. subst.
+      by induction k; simpl; repeat case_decide; simpl;
+        auto using prefix_of_nil, prefix_of_cons.
+    Qed.
+    Lemma max_prefix_of_max_alt (l1 l2 : list A) k1 k2 k3 k :
+      max_prefix_of l1 l2 = (k1,k2,k3) â†’
+      prefix_of k l1 â†’
+      prefix_of k l2 â†’
+      prefix_of k k3.
+    Proof.
+      intro. pose proof (max_prefix_of_max l1 l2 k).
+      by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
+    Qed.
+
+    Lemma max_prefix_of_max_snoc (l1 l2 : list A) k1 k2 k3 x1 x2 :
+      max_prefix_of l1 l2 = (x1 :: k1, x2 :: k2, k3) â†’
+      x1 â‰  x2.
+    Proof.
+      intros Hl ?. subst. destruct (prefix_of_snoc_not k3 x2).
+      eapply max_prefix_of_max_alt; eauto.
+      * rewrite (max_prefix_of_fst_alt _ _ _ _ _ Hl).
+        apply prefix_of_app, prefix_of_cons, prefix_of_nil.
+      * rewrite (max_prefix_of_snd_alt _ _ _ _ _ Hl).
+        apply prefix_of_app, prefix_of_cons, prefix_of_nil.
+    Qed.
+  End prefix_ops.
+
+  Lemma prefix_suffix_reverse (l1 l2 : list A) :
+    prefix_of l1 l2 â†” suffix_of (reverse l1) (reverse l2).
   Proof.
-    induction 1; simpl; constructor; trivial.
-    rewrite elem_of_list_fmap. intros [y [Hxy ?]].
-    apply (injective f) in Hxy. by subst.
+    split; intros [k E]; exists (reverse k).
+    * by rewrite E, reverse_app.
+    * by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
   Qed.
-  Lemma NoDup_fmap `{!Injective (=) (=) f} (l : list A) :
-    NoDup (f <$> l) â†” NoDup l.
-  Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
+  Lemma suffix_prefix_reverse (l1 l2 : list A) :
+    suffix_of l1 l2 â†” prefix_of (reverse l1) (reverse l2).
+  Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
 
-  Global Instance fmap_Permutation_proper:
-    Proper (Permutation ==> Permutation) (fmap f).
-  Proof. induction 1; simpl; econstructor; eauto. Qed.
+  Lemma suffix_of_nil (l : list A) : suffix_of [] l.
+  Proof. exists l. by rewrite (right_id [] (++)). Qed.
+  Lemma suffix_of_nil_inv (l : list A) : suffix_of l [] â†’ l = [].
+  Proof. by intros [[|?] ?]; simplify_list_equality. Qed.
+  Lemma suffix_of_cons_nil_inv x (l : list A) : Â¬suffix_of (x :: l) [].
+  Proof. by intros [[] ?]. Qed.
+  Lemma suffix_of_snoc (l1 l2 : list A) x :
+    suffix_of l1 l2 â†’ suffix_of (l1 ++ [x]) (l2 ++ [x]).
+  Proof. intros [k E]. exists k. subst. by rewrite (associative (++)). Qed.
+  Lemma suffix_of_snoc_alt x y (l1 l2 : list A) :
+    x = y â†’ suffix_of l1 l2 â†’ suffix_of (l1 ++ [x]) (l2 ++ [y]).
+  Proof. intro. subst. apply suffix_of_snoc. Qed.
 
-  Lemma Forall_fmap (l : list A) (P : B â†’ Prop) :
-    Forall P (f <$> l) â†” Forall (P âˆ˜ f) l.
-  Proof.
-    split; induction l; inversion_clear 1; constructor; auto.
-  Qed.
+  Lemma suffix_of_app (l1 l2 k : list A) :
+    suffix_of l1 l2 â†’ suffix_of (l1 ++ k) (l2 ++ k).
+  Proof. intros [k' E]. exists k'. subst. by rewrite (associative (++)). Qed.
+  Lemma suffix_of_app_alt (l1 l2 k1 k2 : list A) :
+    k1 = k2 â†’ suffix_of l1 l2 â†’ suffix_of (l1 ++ k1) (l2 ++ k2).
+  Proof. intro. subst. apply suffix_of_app. Qed.
 
-  Lemma Forall2_fmap_l {C} (P : B â†’ C â†’ Prop) l1 l2 :
-    Forall2 P (f <$> l1) l2 â†” Forall2 (P âˆ˜ f) l1 l2.
+  Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) :
+    suffix_of (l1 ++ [x]) (l2 ++ [y]) â†’ x = y.
   Proof.
-    split; revert l2; induction l1; inversion_clear 1; constructor; auto.
+    rewrite suffix_prefix_reverse, !reverse_snoc.
+    by apply prefix_of_cons_inv_1.
   Qed.
-  Lemma Forall2_fmap_r {C} (P : C â†’ B â†’ Prop) l1 l2 :
-    Forall2 P l1 (f <$> l2) â†” Forall2 (Î» x, P x âˆ˜ f) 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.
-    split; revert l1; induction l2; inversion_clear 1; constructor; auto.
+    rewrite !suffix_prefix_reverse, !reverse_snoc.
+    by apply prefix_of_cons_inv_2.
   Qed.
-  Lemma Forall2_fmap_1 {C D} (g : C â†’ D) (P : B â†’ D â†’ Prop) l1 l2 :
-    Forall2 P (f <$> l1) (g <$> l2) â†’
-    Forall2 (Î» x1 x2, P (f x1) (g x2)) l1 l2.
-  Proof. revert l2; induction l1; intros [|??]; inversion_clear 1; auto. Qed.
-  Lemma Forall2_fmap_2 {C D} (g : C â†’ D) (P : B â†’ D â†’ Prop) l1 l2 :
-    Forall2 (Î» x1 x2, P (f x1) (g x2)) l1 l2 â†’
-    Forall2 P (f <$> l1) (g <$> l2).
-  Proof. induction 1; simpl; auto. Qed.
-  Lemma Forall2_fmap {C D} (g : C â†’ D) (P : B â†’ D â†’ Prop) l1 l2 :
-    Forall2 P (f <$> l1) (g <$> l2) â†”
-    Forall2 (Î» x1 x2, P (f x1) (g x2)) l1 l2.
-  Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.
 
-  Lemma mapM_fmap_Some (g : B â†’ option A) (l : list A) :
-    (âˆ€ x, g (f x) = Some x) â†’
-    mapM g (f <$> l) = Some l.
-  Proof. intros. by induction l; simpl; simplify_option_equality. Qed.
-  Lemma mapM_fmap_Some_inv (g : B â†’ option A) (l : list A) (k : list B) :
-    (âˆ€ x y, g y = Some x â†’ y = f x) â†’
-    mapM g k = Some l â†’
-    k = f <$> l.
+  Lemma suffix_of_cons_l (l1 l2 : list A) x :
+    suffix_of (x :: l1) l2 â†’ suffix_of l1 l2.
   Proof.
-    intros Hgf. revert l; induction k as [|y k]; intros [|x l] ?;
-      simplify_option_equality; f_equiv; eauto.
+    intros [k ?]. exists (k ++ [x]). subst.
+    by rewrite <-(associative (++)).
   Qed.
-
-  Lemma mapM_Some (g : B â†’ option A) l k :
-    Forall2 (Î» x y, g x = Some y) l k â†’
-    mapM g l = Some k.
-  Proof. by induction 1; simplify_option_equality. Qed.
-
-  Lemma Forall2_impl_mapM (P : B â†’ A â†’ Prop) (g : B â†’ option A) l k :
-    Forall (Î» x, âˆ€ y, g x = Some y â†’ P x y) l â†’
-    mapM g l = Some k â†’
-    Forall2 P l k.
+  Lemma suffix_of_app_l (l1 l2 l3 : list A) :
+    suffix_of (l3 ++ l1) l2 â†’ suffix_of l1 l2.
   Proof.
-    intros Hl. revert k. induction Hl; intros [|??] ?;
-      simplify_option_equality; eauto.
+    intros [k ?]. exists (k ++ l3). subst.
+    by rewrite <-(associative (++)).
   Qed.
-End list_fmap.
-
-Lemma NoDup_fmap_fst {A B} (l : list (A * B)) :
-  (âˆ€ x y1 y2, (x,y1) âˆˆ l â†’ (x,y2) âˆˆ l â†’ y1 = y2) â†’
-  NoDup l â†’
-  NoDup (fst <$> l).
-Proof.
-  intros Hunique.
-  induction 1 as [|[x1 y1] l Hin Hnodup IH]; simpl; constructor.
-  * rewrite elem_of_list_fmap.
-    intros [[x2 y2] [??]]; simpl in *; subst. destruct Hin.
-    rewrite (Hunique x2 y1 y2); rewrite ?elem_of_cons; auto.
-  * apply IH. intros.
-    eapply Hunique; rewrite ?elem_of_cons; eauto.
-Qed.
-
-Section list_bind.
-  Context {A B : Type} (f : A â†’ list B).
-
-  Lemma bind_app (l1 l2 : list A) :
-    (l1 ++ l2) â‰«= f = (l1 â‰«= f) ++ (l2 â‰«= f).
+  Lemma suffix_of_cons_r (l1 l2 : list A) x :
+    suffix_of l1 l2 â†’ suffix_of l1 (x :: l2).
+  Proof. intros [k ?]. exists (x :: k). by subst. Qed.
+  Lemma suffix_of_app_r (l1 l2 l3 : list A) :
+    suffix_of l1 l2 â†’ suffix_of l1 (l3 ++ l2).
   Proof.
-    induction l1; simpl; [done|].
-    by rewrite <-(associative (++)), IHl1.
+    intros [k ?]. exists (l3 ++ k). subst.
+    by rewrite (associative (++)).
   Qed.
-  Lemma elem_of_list_bind (x : B) (l : list A) :
-    x âˆˆ l â‰«= f â†” âˆƒ y, x âˆˆ f y âˆ§ y âˆˆ l.
+
+  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.
-    split.
-    * induction l as [|y l IH]; simpl; intros; decompose_elem_of_list.
-      + exists y. split; [done | by left].
-      + destruct IH as [z [??]]. done.
-        exists z. split; [done | by right].
-    * intros [y [Hx Hy]].
-      induction Hy; simpl; rewrite elem_of_app; intuition.
+    intros [[|? k] E].
+    * by left.
+    * right. simplify_equality. by apply suffix_of_app_r.
   Qed.
 
-  Lemma Forall2_bind {C D} (g : C â†’ list D) (P : B â†’ D â†’ Prop) l1 l2 :
-    Forall2 (Î» x1 x2, Forall2 P (f x1) (g x2)) l1 l2 â†’
-    Forall2 P (l1 â‰«= f) (l2 â‰«= g).
-  Proof. induction 1; simpl; auto using Forall2_app. Qed.
-End list_bind.
-
-Section list_ret_join.
-  Context {A : Type}.
-
-  Lemma list_join_bind (ls : list (list A)) :
-    mjoin ls = ls â‰«= id.
-  Proof. induction ls; simpl; f_equal; auto. Qed.
-
-  Lemma elem_of_list_ret (x y : A) :
-    x âˆˆ @mret list _ A y â†” x = y.
-  Proof. apply elem_of_list_singleton. Qed.
-  Lemma elem_of_list_join (x : A) (ls : list (list A)) :
-    x âˆˆ mjoin ls â†” âˆƒ l, x âˆˆ l âˆ§ l âˆˆ ls.
-  Proof. by rewrite list_join_bind, elem_of_list_bind. Qed.
+  Lemma suffix_of_length (l1 l2 : list A) :
+    suffix_of l1 l2 â†’ length l1 â‰¤ length l2.
+  Proof. intros [??]. subst. rewrite app_length. lia. Qed.
+  Lemma suffix_of_cons_not x (l : list A) : Â¬suffix_of (x :: l) l.
+  Proof. intros [??]. discriminate_list_equality. Qed.
 
-  Lemma join_nil (ls : list (list A)) :
-    mjoin ls = [] â†” Forall (= []) ls.
+  Global Instance suffix_of_dec `{âˆ€ x y : A, Decision (x = y)}
+    (l1 l2 : list A) : Decision (suffix_of l1 l2).
   Proof.
-    split.
-    * by induction ls as [|[|??] ?]; constructor; auto.
-    * by induction 1 as [|[|??] ?].
-  Qed.
-  Lemma join_nil_1 (ls : list (list A)) :
-    mjoin ls = [] â†’ Forall (= []) ls.
-  Proof. by rewrite join_nil. Qed.
-  Lemma join_nil_2 (ls : list (list A)) :
-    Forall (= []) ls â†’ mjoin ls = [].
-  Proof. by rewrite join_nil. Qed.
+    refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
+     abstract (by rewrite suffix_prefix_reverse).
+  Defined.
 
-  Lemma join_length (ls : list (list A)) :
-    length (mjoin ls) = foldr (plus âˆ˜ length) 0 ls.
-  Proof. by induction ls; simpl; rewrite ?app_length; f_equal. Qed.
-  Lemma join_length_same (ls : list (list A)) n :
-    Forall (Î» l, length l = n) ls â†’
-    length (mjoin ls) = length ls * n.
-  Proof. rewrite join_length. by induction 1; simpl; f_equal. Qed.
+  Section max_suffix_of.
+    Context `{âˆ€ x y : A, Decision (x = y)}.
 
-  Lemma lookup_join_same_length (ls : list (list A)) n i :
-    n â‰  0 â†’
-    Forall (Î» l, length l = n) ls â†’
-    mjoin ls !! i = ls !! (i `div` n) â‰«= (!! (i `mod` n)).
-  Proof.
-    intros Hn Hls. revert i.
-    induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
-    destruct (decide (i < n)) as [Hin|Hin].
-    * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
-      rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
-      simpl. rewrite lookup_app_l; auto with lia.
-    * replace i with ((i - n) + 1 * n) by lia.
-      rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
-      replace (i - n + 1 * n) with i by lia.
-      rewrite (plus_comm _ 1), lookup_app_r_alt, IH by lia.
-      by subst.
-  Qed.
+    Lemma max_suffix_of_fst (l1 l2 : list A) :
+      l1 = fst (fst (max_suffix_of l1 l2)) ++ snd (max_suffix_of l1 l2).
+    Proof.
+      rewrite <-(reverse_involutive l1) at 1.
+      rewrite (max_prefix_of_fst (reverse l1) (reverse l2)).
+      unfold max_suffix_of.
+      destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
+      by rewrite reverse_app.
+    Qed.
+    Lemma max_suffix_of_fst_alt (l1 l2 : list A) k1 k2 k3 :
+      max_suffix_of l1 l2 = (k1,k2,k3) â†’ l1 = k1 ++ k3.
+    Proof.
+      intro. pose proof (max_suffix_of_fst l1 l2).
+      by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
+    Qed.
+    Lemma max_suffix_of_fst_suffix (l1 l2 : list A) :
+      suffix_of (snd (max_suffix_of l1 l2)) l1.
+    Proof. eexists. apply max_suffix_of_fst. Qed.
+    Lemma max_suffix_of_fst_suffix_alt (l1 l2 : list A) k1 k2 k3 :
+      max_suffix_of l1 l2 = (k1,k2,k3) â†’ suffix_of k3 l1.
+    Proof. eexists. eauto using max_suffix_of_fst_alt. Qed.
 
-  (* This should be provable using the previous lemma in a shorter way *)
-  Lemma alter_join_same_length f (ls : list (list A)) n i :
-    n â‰  0 â†’
-    Forall (Î» l, length l = n) ls â†’
-    alter f i (mjoin ls) = mjoin (alter (alter f (i `mod` n)) (i `div` n) ls).
-  Proof.
-    intros Hn Hls. revert i.
-    induction Hls as [|l ls ? Hls IH]; simpl; [done |]. intros i.
-    destruct (decide (i < n)) as [Hin|Hin].
-    * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
-      rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
-      simpl. rewrite alter_app_l; auto with lia.
-    * replace i with ((i - n) + 1 * n) by lia.
-      rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
-      replace (i - n + 1 * n) with i by lia.
-      rewrite (plus_comm _ 1), alter_app_r_alt, IH by lia.
-      by subst.
-  Qed.
-  Lemma insert_join_same_length (ls : list (list A)) n i x :
-    n â‰  0 â†’
-    Forall (Î» l, length l = n) ls â†’
-    <[i:=x]>(mjoin ls) = mjoin (alter <[i `mod` n:=x]> (i `div` n) ls).
-  Proof. apply alter_join_same_length. Qed.
+    Lemma max_suffix_of_snd (l1 l2 : list A) :
+      l2 = snd (fst (max_suffix_of l1 l2)) ++ snd (max_suffix_of l1 l2).
+    Proof.
+      rewrite <-(reverse_involutive l2) at 1.
+      rewrite (max_prefix_of_snd (reverse l1) (reverse l2)).
+      unfold max_suffix_of.
+      destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
+      by rewrite reverse_app.
+    Qed.
+    Lemma max_suffix_of_snd_alt (l1 l2 : list A) k1 k2 k3 :
+      max_suffix_of l1 l2 = (k1,k2,k3) â†’ l2 = k2 ++ k3.
+    Proof.
+      intro. pose proof (max_suffix_of_snd l1 l2).
+      by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
+    Qed.
+    Lemma max_suffix_of_snd_suffix (l1 l2 : list A) :
+      suffix_of (snd (max_suffix_of l1 l2)) l2.
+    Proof. eexists. apply max_suffix_of_snd. Qed.
+    Lemma max_suffix_of_snd_suffix_alt (l1 l2 : list A) k1 k2 k3 :
+      max_suffix_of l1 l2 = (k1,k2,k3) â†’ suffix_of k3 l2.
+    Proof. eexists. eauto using max_suffix_of_snd_alt. Qed.
 
-  Lemma Forall2_join {B} (P : A â†’ B â†’ Prop) ls1 ls2 :
-    Forall2 (Forall2 P) ls1 ls2 â†’
-    Forall2 P (mjoin ls1) (mjoin ls2).
-  Proof. induction 1; simpl; auto using Forall2_app. Qed.
-End list_ret_join.
+    Lemma max_suffix_of_max (l1 l2 : list A) k :
+      suffix_of k l1 â†’
+      suffix_of k l2 â†’
+      suffix_of k (snd (max_suffix_of l1 l2)).
+    Proof.
+      generalize (max_prefix_of_max (reverse l1) (reverse l2)).
+      rewrite !suffix_prefix_reverse. unfold max_suffix_of.
+      destruct (max_prefix_of (reverse l1) (reverse l2)) as ((?&?)&?); simpl.
+      rewrite reverse_involutive. auto.
+    Qed.
+    Lemma max_suffix_of_max_alt (l1 l2 : list A) k1 k2 k3 k :
+      max_suffix_of l1 l2 = (k1,k2,k3) â†’
+      suffix_of k l1 â†’
+      suffix_of k l2 â†’
+      suffix_of k k3.
+    Proof.
+      intro. pose proof (max_suffix_of_max l1 l2 k).
+      by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
+    Qed.
 
-Ltac simplify_list_fmap_equality := repeat
-  match goal with
-  | _ => progress simplify_equality
-  | H : _ <$> _ = [] |- _ => apply fmap_nil_inv in H
-  | H : [] = _ <$> _ |- _ => symmetry in H; apply fmap_nil_inv in H
-  | H : _ <$> _ = _ :: _ |- _ =>
-     apply fmap_cons_inv in H; destruct H as (?&?&?&?&?)
-  | H : _ :: _ = _ <$> _ |- _ => symmetry in H
-  | H : _ <$> _ = _ ++ _ |- _ =>
-     apply fmap_app_inv in H; destruct H as (?&?&?&?&?)
-  | H : _ ++ _ = _ <$> _ |- _ => symmetry in H
-  end.
+    Lemma max_suffix_of_max_snoc (l1 l2 : list A) k1 k2 k3 x1 x2 :
+      max_suffix_of l1 l2 = (k1 ++ [x1], k2 ++ [x2], k3) â†’
+      x1 â‰  x2.
+    Proof.
+      intros Hl ?. subst. destruct (suffix_of_cons_not x2 k3).
+      eapply max_suffix_of_max_alt; eauto.
+      * rewrite (max_suffix_of_fst_alt _ _ _ _ _ Hl).
+        by apply (suffix_of_app [x2]), suffix_of_app_r.
+      * rewrite (max_suffix_of_snd_alt _ _ _ _ _ Hl).
+        by apply (suffix_of_app [x2]), suffix_of_app_r.
+    Qed.
+  End max_suffix_of.
+End prefix_postfix.
 
-(** * Indexed folds and maps *)
-(** We define stronger variants of map and fold that also take the index of the
-element into account. *)
-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.
+(** ** Properties of the folding functions *)
+Notation foldr_app := fold_right_app.
+Lemma foldl_app {A B} (f : A â†’ B â†’ A) (l k : list B) (a : A) :
+  foldl f a (l ++ k) = foldl f (foldl f a l) k.
+Proof. revert a. induction l; simpl; auto. Qed.
 
-Definition ifoldr {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 foldr_permutation {A B} (R : relation B)
+   `{!Equivalence R}
+   (f : A â†’ B â†’ B) (b : B)
+   `{!Proper ((=) ==> R ==> R) f}
+   (Hf : âˆ€ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
+  Proper (Permutation ==> R) (foldr f b).
+Proof.
+  induction 1; simpl.
+  * done.
+  * by f_equiv.
+  * apply Hf.
+  * etransitivity; eauto.
+Qed.
 
 Lemma ifoldr_app {A B} (f : nat â†’ B â†’ A â†’ A) (a : nat â†’ A)
     (l1 l2 : list B) n :
@@ -2144,75 +2201,7 @@ Proof.
   revert n a. induction l1 as [| b l1 IH ]; intros; simpl; f_equal; auto.
 Qed.
 
-(** * Lists of the same length *)
-(** The [same_length] view allows convenient induction over two lists with the
-same length. *)
-Section same_length.
-  Context {A B : Type}.
-
-  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_1 l k :
-    same_length l k â†’ length l = length k.
-  Proof. induction 1; simpl; auto. Qed.
-  Lemma same_length_length_2 l k :
-    length l = length k â†’ same_length l k.
-  Proof.
-    revert k. induction l; intros [|??]; try discriminate;
-      constructor; auto with arith.
-  Qed.
-  Lemma same_length_length l k :
-    same_length l k â†” length l = length k.
-  Proof. split; auto using same_length_length_1, same_length_length_2. Qed.
-
-  Lemma same_length_lookup l k i :
-    same_length l k â†’ is_Some (l !! i) â†’ is_Some (k !! i).
-  Proof.
-    rewrite same_length_length.
-    setoid_rewrite lookup_lt_length.
-    intros E. by rewrite E.
-  Qed.
-
-  Lemma Forall2_same_length (P : A â†’ B â†’ Prop) l1 l2 :
-    Forall2 P l1 l2 â†’
-    same_length l1 l2.
-  Proof. intro. eapply same_length_length, Forall2_length; eauto. Qed.
-  Lemma Forall2_app_inv (P : A â†’ B â†’ Prop) l1 l2 k1 k2 :
-    same_length l1 k1 â†’
-    Forall2 P (l1 ++ l2) (k1 ++ k2) â†’ Forall2 P l2 k2.
-  Proof. induction 1. done. inversion 1; subst; auto. Qed.
-
-  Lemma same_length_Forall2 l1 l2 :
-    same_length l1 l2 â†” Forall2 (Î» _ _, True) l1 l2.
-  Proof. split; induction 1; constructor; auto. Qed.
-
-  Lemma same_length_take l1 l2 n :
-    same_length l1 l2 â†’
-    same_length (take n l1) (take n l2).
-  Proof. rewrite !same_length_Forall2. apply Forall2_take. Qed.
-  Lemma same_length_drop l1 l2 n :
-    same_length l1 l2 â†’
-    same_length (drop n l1) (drop n l2).
-  Proof. rewrite !same_length_Forall2. apply Forall2_drop. Qed.
-  Lemma same_length_resize l1 l2 x1 x2 n :
-    same_length (resize n x1 l1) (resize n x2 l2).
-  Proof. apply same_length_length. by rewrite !resize_length. Qed.
-End same_length.
-
-Instance: âˆ€ A, Reflexive (@same_length A A).
-Proof. intros A l. induction l; constructor; auto. Qed.
-
-(** * Zipping lists *)
-Definition zip_with {A B C} (f : A â†’ B â†’ C) : list A â†’ list B â†’ list C :=
-  fix go l1 l2 :=
-  match l1, l2 with
-  | x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2
-  | _ , _ => []
-  end.
-
+(** ** Properties of the [zip_with] and [zip] functions *)
 Section zip_with.
   Context {A B C : Type} (f : A â†’ B â†’ C).
 
@@ -2310,8 +2299,6 @@ Section zip_with.
   Qed.
 End zip_with.
 
-Notation zip := (zip_with pair).
-
 Section zip.
   Context {A B : Type}.
 
@@ -2338,21 +2325,6 @@ Section zip.
   Proof. by apply zip_with_fmap_snd. Qed.
 End zip.
 
-Ltac simplify_zip_equality := repeat
-  match goal with
-  | _ => progress simplify_equality
-  | H : zip_with _ _ _ = [] |- _ =>
-     apply zip_with_nil_inv in H; destruct H
-  | H : [] = zip_with _ _ _ |- _ =>
-     symmetry in H
-  | H : zip_with _ _ _ = _ :: _ |- _ =>
-    apply zip_with_cons_inv in H; destruct H as (?&?&?&?&?&?&?&?)
-  | H : _ :: _ = zip_with _ _ _ |- _ => symmetry in H
-  | H : zip_with _ _ _ = _ ++ _ |- _ =>
-     apply zip_with_app_inv in H; destruct H as (?&?&?&?&?&?&?&?)
-  | H : _ ++ _ = zip_with _ _ _ |- _ => symmetry in H
-  end.
-
 Definition zipped_map {A B} (f : list A â†’ list A â†’ A â†’ B) :
     list A â†’ list A â†’ list B :=
   fix go l k :=
@@ -2366,8 +2338,7 @@ Lemma elem_of_zipped_map {A B} (f : list A â†’ list A â†’ A â†’ B) l k x :
     âˆƒ k' k'' y, k = k' ++ [y] ++ k'' âˆ§ x = f (reverse k' ++ l) k'' y.
 Proof.
   split.
-  * revert l. induction k as [|z k IH]; simpl;
-      intros l ?; decompose_elem_of_list.
+  * revert l. induction k as [|z k IH]; simpl; intros l; inversion_clear 1.
     + by eexists [], k, z.
     + destruct (IH (z :: l)) as [k' [k'' [y [??]]]]; [done |]; subst.
       eexists (z :: k'), k'', y. split; [done |].
@@ -2408,18 +2379,7 @@ Proof.
   by apply IH.
 Qed.
 
-(** * Permutations *)
-Fixpoint interleave {A} (x : A) (l : list A) : list (list A) :=
-  match l with
-  | [] => [ [x] ]
-  | y :: l => (x :: y :: l) :: ((y ::) <$> interleave x l)
-  end.
-Fixpoint permutations {A} (l : list A) : list (list A) :=
-  match l with
-  | [] => [ [] ]
-  | x :: l => permutations l â‰«= interleave x
-  end.
-
+(** ** Permutations *)
 Section permutations.
   Context {A : Type}.
 
@@ -2629,3 +2589,138 @@ Section list_set_operations.
         case_match; simpl; rewrite ?elem_of_cons; auto.
   Qed.
 End list_set_operations.
+
+(** * Tactics *)
+Ltac decompose_elem_of_list := repeat
+  match goal with
+  | H : ?x âˆˆ [] |- _ => by destruct (not_elem_of_nil x)
+  | H : _ âˆˆ _ :: _ |- _ => apply elem_of_cons in H; destruct H
+  | H : _ âˆˆ _ ++ _ |- _ => apply elem_of_app in H; destruct H
+  end.
+
+Ltac simplify_list_fmap_equality := repeat
+  match goal with
+  | _ => progress simplify_equality
+  | H : _ <$> _ = [] |- _ => apply fmap_nil_inv in H
+  | H : [] = _ <$> _ |- _ => symmetry in H; apply fmap_nil_inv in H
+  | H : _ <$> _ = _ :: _ |- _ =>
+     apply fmap_cons_inv in H; destruct H as (?&?&?&?&?)
+  | H : _ :: _ = _ <$> _ |- _ => symmetry in H
+  | H : _ <$> _ = _ ++ _ |- _ =>
+     apply fmap_app_inv in H; destruct H as (?&?&?&?&?)
+  | H : _ ++ _ = _ <$> _ |- _ => symmetry in H
+  end.
+
+Ltac simplify_zip_equality := repeat
+  match goal with
+  | _ => progress simplify_equality
+  | H : zip_with _ _ _ = [] |- _ =>
+     apply zip_with_nil_inv in H; destruct H
+  | H : [] = zip_with _ _ _ |- _ =>
+     symmetry in H
+  | H : zip_with _ _ _ = _ :: _ |- _ =>
+    apply zip_with_cons_inv in H; destruct H as (?&?&?&?&?&?&?&?)
+  | H : _ :: _ = zip_with _ _ _ |- _ => symmetry in H
+  | H : zip_with _ _ _ = _ ++ _ |- _ =>
+     apply zip_with_app_inv in H; destruct H as (?&?&?&?&?&?&?&?)
+  | H : _ ++ _ = zip_with _ _ _ |- _ => symmetry in H
+  end.
+
+Ltac decompose_Forall_hyps := repeat
+  match goal with
+  | H : Forall _ [] |- _ => inversion H
+  | H : Forall _ (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
+  | H : Forall _ (_ ++ _) |- _ => rewrite Forall_app in H; destruct H
+  | H : Forall _ (_ <$> _) |- _ => rewrite Forall_fmap in H
+  | H : Forall2 _ [] [] |- _ => clear H
+  | H : Forall2 _ (_ :: _) [] |- _ => destruct (Forall2_cons_nil_inv _ _ _ H)
+  | H : Forall2 _ [] (_ :: _) |- _ => destruct (Forall2_nil_cons_inv _ _ _ H)
+  | H : Forall2 _ [] ?l |- _ => apply Forall2_nil_inv_l in H; subst l
+  | H : Forall2 _ ?l [] |- _ => apply Forall2_nil_inv_r in H; subst l
+  | H : Forall2 _ (_ :: _) (_ :: _) |- _ =>
+     apply Forall2_cons_inv in H; destruct H
+  | H : Forall2 _ (_ :: _) ?l |- _ =>
+     apply Forall2_cons_inv_l in H; destruct H as (? & ? & ? & ? & ?); subst l
+  | H : Forall2 _ ?l (_ :: _) |- _ =>
+     apply Forall2_cons_inv_r in H; destruct H as (? & ? & ? & ? & ?); subst l
+  | H : Forall2 _ (_ ++ _) (_ ++ _) |- _ =>
+     destruct (Forall2_app_inv _ _ _ _ _ H); [eauto using Forall2_same_length |]
+  | H : Forall2 _ (_ ++ _) ?l |- _ =>
+     apply Forall2_app_inv_l in H; destruct H as (? & ? & ? & ? & ?); subst l
+  | H : Forall2 _ ?l (_ ++ _) |- _ =>
+     apply Forall2_app_inv_r in H; destruct H as (? & ? & ? & ? & ?); subst l
+  | H : Forall ?P ?l, H1 : ?l !! _ = Some ?x |- _ =>
+    unless (P x) by done;
+    let E := fresh in
+    assert (P x) as E by (apply (Forall_lookup_1 P _ _ _ H H1));
+    lazy beta in E
+  | _ =>
+    lazymatch goal with
+    | H : Forall2 ?P ?l1 ?l2, H1 : ?l1 !! ?i = Some ?x,
+                              H2 : ?l2 !! ?i = Some ?y |- _ =>
+      unless (P x y) by done;
+      let E := fresh in
+      assert (P x y) as E by (apply (Forall2_lookup_lr P _ _ _ _ _ H H1 H2));
+     lazy beta in E
+    | H : Forall2 ?P ?l1 _, H1 : ?l1 !! _ = Some ?x |- _ =>
+      destruct (Forall2_lookup_l P _ _ _ _ H H1) as (?&?&?)
+    | H : Forall2 ?P _ ?l2, H2 : ?l2 !! _ = Some ?y |- _ =>
+      destruct (Forall2_lookup_r P _ _ _ _ H H2) as (?&?&?)
+    end
+  end.
+Ltac decompose_Forall := repeat
+  match goal with
+  | |- Forall _ _ => by apply Forall_true
+  | |- Forall _ [] => constructor
+  | |- Forall _ (_ :: _) => constructor
+  | |- Forall _ (_ ++ _) => apply Forall_app
+  | |- Forall _ (_ <$> _) => apply Forall_fmap
+  | |- Forall2 _ _ _ => apply Forall2_Forall
+  | |- Forall2 _ [] [] => constructor
+  | |- Forall2 _ (_ :: _) (_ :: _) => constructor
+  | |- Forall2 _ (_ ++ _) (_ ++ _) => first
+    [ apply Forall2_app; [by decompose_Forall |]
+    | apply Forall2_app; [| by decompose_Forall]]
+  | |- Forall2 _ (_ <$> _) _ => apply Forall2_fmap_l
+  | |- Forall2 _ _ (_ <$> _) => apply Forall2_fmap_r
+  | _ => progress decompose_Forall_hyps
+  | |- Forall _ _ =>
+    apply Forall_lookup_2;
+    intros ???; progress decompose_Forall_hyps
+  | |- Forall2 _ _ _ =>
+    apply Forall2_lookup_2; [by eauto using Forall2_same_length|];
+    intros ?????; progress decompose_Forall_hyps
+  end.
+
+(** The [simplify_suffix_of] tactic removes [suffix_of] hypotheses that are
+tautologies, and simplifies [suffix_of] hypotheses involving [(::)] and
+[(++)]. *)
+Ltac simplify_suffix_of := repeat
+  match goal with
+  | H : suffix_of (_ :: _) _ |- _ =>
+    destruct (suffix_of_cons_not _ _ H)
+  | H : suffix_of (_ :: _) [] |- _ =>
+    apply suffix_of_nil_inv in 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_equality
+  end.
+
+(** The [solve_suffix_of] tactic tries to solve goals involving [suffix_of]. It
+uses [simplify_suffix_of] to simplify hypotheses and tries to solve [suffix_of]
+conclusions. This tactic either fails or proves the goal. *)
+Ltac solve_suffix_of := solve [intuition (repeat
+  match goal with
+  | _ => done
+  | _ => progress simplify_suffix_of
+  | |- suffix_of [] _ => apply suffix_of_nil
+  | |- suffix_of _ _ => reflexivity
+  | |- suffix_of _ (_ :: _) => apply suffix_of_cons_r
+  | |- suffix_of _ (_ ++ _) => apply suffix_of_app_r
+  | H : suffix_of _ _ â†’ False |- _ => destruct H
+  end)].
+Hint Extern 0 (PropHolds (suffix_of _ _)) =>
+  unfold PropHolds; solve_suffix_of : typeclass_instances.
diff --git a/theories/mapset.v b/theories/mapset.v
index 25b7d40d9d6256910ed445e15f71d10ea4be5438..6c2bd438e1281e862883ac0967e2c04c13d80b7b 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -47,9 +47,14 @@ Proof.
     apply option_eq. intros []. by apply E.
 Qed.
 
-Global Instance mapset_eq_dec `{âˆ€ m1 m2 : M unit, Decision (m1 = m2)} :
-  âˆ€ X1 X2 : mapset M, Decision (X1 = X2) | 1.
-Proof. solve_decision. Defined.
+Global Instance mapset_eq_dec `{âˆ€ m1 m2 : M unit, Decision (m1 = m2)}
+    (X1 X2 : mapset M) : Decision (X1 = X2) | 1.
+Proof.
+ refine
+  match X1, X2 with
+  | Mapset m1, Mapset m2 => cast_if (decide (m1 = m2))
+  end; abstract congruence.
+Defined.
 Global Instance mapset_elem_of_dec x (X : mapset M) :
   Decision (x âˆˆ X) | 1.
 Proof. solve_decision. Defined.
diff --git a/theories/nmap.v b/theories/nmap.v
index 8fac809aa29c49311780f2a41ca0859026374d50..a2abeeaf683b422493defa55cce955a55886be8a 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -12,9 +12,15 @@ Arguments Nmap_0 {_} _.
 Arguments Nmap_pos {_} _.
 Arguments NMap {_} _ _.
 
-Instance Pmap_dec `{âˆ€ x y : A, Decision (x = y)} :
-  âˆ€ x y : Nmap A, Decision (x = y).
-Proof. solve_decision. Defined.
+Instance Nmap_eq_dec `{âˆ€ x y : A, Decision (x = y)} (t1 t2 : Nmap A) :
+  Decision (t1 = t2).
+Proof.
+ refine
+  match t1, t2 with
+  | NMap x t1, NMap y t2 =>
+    cast_if_and (decide (x = y)) (decide (t1 = t2))
+  end; abstract congruence.
+Defined.
 
 Instance Nempty {A} : Empty (Nmap A) := NMap None âˆ….
 Instance Nlookup {A} : Lookup N A (Nmap A) := Î» i t,
diff --git a/theories/option.v b/theories/option.v
index 22847c93c471d45ab69397a880c5d08aa5c10d3a..af77b0034bbe287eced6df3f8d0202a6c1a7be8b 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -122,6 +122,14 @@ Instance option_fmap: FMap option := @option_map.
 Instance option_guard: MGuard option := Î» P dec A x,
   if dec then x else None.
 
+Definition mapM `{!MBind M} `{!MRet M} {A B}
+    (f : A â†’ M B) : list A â†’ M (list B) :=
+  fix go l :=
+  match l with
+  | [] => mret []
+  | x :: l => y â† f x; k â† go l; mret (y :: k)
+  end.
+
 Lemma fmap_is_Some {A B} (f : A â†’ B) (x : option A) :
   is_Some (f <$> x) â†” is_Some x.
 Proof. split; inversion 1. by destruct x. done. Qed.
@@ -138,6 +146,51 @@ Proof. by destruct x. Qed.
 Lemma option_bind_assoc {A B C} (f : A â†’ option B)
     (g : B â†’ option C) (x : option A) : (x â‰«= f) â‰«= g = x â‰«= (mbind g âˆ˜ f).
 Proof. by destruct x; simpl. Qed.
+Lemma option_bind_ext {A B} (f g : A â†’ option B) x y :
+  (âˆ€ a, f a = g a) â†’
+  x = y â†’
+  x â‰«= f = y â‰«= g.
+Proof. intros. destruct x, y; simplify_equality; simpl; auto. Qed.
+Lemma option_bind_ext_fun {A B} (f g : A â†’ option B) x :
+  (âˆ€ a, f a = g a) â†’
+  x â‰«= f = x â‰«= g.
+Proof. intros. by apply option_bind_ext. Qed.
+
+Section mapM.
+  Context {A B : Type} (f : A â†’ option B).
+
+  Lemma mapM_ext (g : A â†’ option B) l :
+    (âˆ€ x, f x = g x) â†’ mapM f l = mapM g l.
+  Proof. intros Hfg. by induction l; simpl; rewrite ?Hfg, ?IHl. Qed.
+  Lemma Forall2_mapM_ext (g : A â†’ option B) l k :
+    Forall2 (Î» x y, f x = g y) l k â†’ mapM f l = mapM g k.
+  Proof.
+    induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH.
+  Qed.
+  Lemma Forall_mapM_ext (g : A â†’ option B) l :
+    Forall (Î» x, f x = g x) l â†’ mapM f l = mapM g l.
+  Proof.
+    induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH.
+  Qed.
+
+  Lemma mapM_Some_1 l k :
+    mapM f l = Some k â†’ Forall2 (Î» x y, f x = Some y) l k.
+  Proof.
+    revert k. induction l as [|x l]; intros [|y k]; simpl; try done.
+    * destruct (f x); simpl; [|discriminate]. by destruct (mapM f l).
+    * destruct (f x) eqn:?; simpl; [|discriminate].
+      destruct (mapM f l); intros; simplify_equality. constructor; auto.
+  Qed.
+  Lemma mapM_Some_2 l k :
+    Forall2 (Î» x y, f x = Some y) l k â†’ mapM f l = Some k.
+  Proof.
+    induction 1 as [|???? Hf ? IH]; simpl; [done |].
+    rewrite Hf. simpl. by rewrite IH.
+  Qed.
+  Lemma mapM_Some l k :
+    mapM f l = Some k â†” Forall2 (Î» x y, f x = Some y) l k.
+  Proof. split; auto using mapM_Some_1, mapM_Some_2. Qed.
+End mapM.
 
 Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
   match goal with
@@ -222,11 +275,13 @@ Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
     assert (y = x) by congruence; clear H2
   | H1 : ?o = Some ?x, H2 : ?o = None |- _ =>
     congruence
+  | H : mapM _ _ = Some _ |- _ => apply mapM_Some in H
   end.
 Tactic Notation "simplify_option_equality" :=
   simplify_option_equality by eauto.
 
-Hint Extern 100 => simplify_option_equality : simplify_option_equality.
+Hint Extern 800 =>
+  progress simplify_option_equality : simplify_option_equality.
 
 (** * Union, intersection and difference *)
 Instance option_union_with {A} : UnionWith A (option A) := Î» f x y,
diff --git a/theories/orders.v b/theories/orders.v
index af0bec44511383fcd134db24e743f05fdb5ef16d..b3ba0df3620d9e9dd2158af4df905215492f71cf 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -209,7 +209,7 @@ Section bounded_join_sl.
         by transitivity (X âˆª Y); [auto | rewrite E].
     * intros [E1 E2]. by rewrite E1, E2, (left_id _ _).
   Qed.
-  Lemma empty_list_union Xs : â‹ƒ Xs â‰¡ âˆ… â†” Forall (â‰¡ âˆ…) Xs.
+  Lemma empty_union_list Xs : â‹ƒ Xs â‰¡ âˆ… â†” Forall (â‰¡ âˆ…) Xs.
   Proof.
     split.
     * induction Xs; simpl; rewrite ?empty_union; intuition.
@@ -248,8 +248,8 @@ Section bounded_join_sl.
 
     Lemma empty_union_L X Y : X âˆª Y = âˆ… â†” X = âˆ… âˆ§ Y = âˆ….
     Proof. unfold_leibniz. apply empty_union. Qed.
-    Lemma empty_list_union_L Xs : â‹ƒ Xs = âˆ… â†” Forall (= âˆ…) Xs.
-    Proof. unfold_leibniz. apply empty_list_union. Qed.
+    Lemma empty_union_list_L Xs : â‹ƒ Xs = âˆ… â†” Forall (= âˆ…) Xs.
+    Proof. unfold_leibniz. apply empty_union_list. Qed.
   End leibniz.
 
   Section dec.
@@ -257,14 +257,14 @@ Section bounded_join_sl.
 
     Lemma non_empty_union X Y : X âˆª Y â‰¢ âˆ… â†’ X â‰¢ âˆ… âˆ¨ Y â‰¢ âˆ….
     Proof. rewrite empty_union. destruct (decide (X â‰¡ âˆ…)); intuition. Qed.
-    Lemma non_empty_list_union Xs : â‹ƒ Xs â‰¢ âˆ… â†’ Exists (â‰¢ âˆ…) Xs.
-    Proof. rewrite empty_list_union. apply (not_Forall_Exists _). Qed.
+    Lemma non_empty_union_list Xs : â‹ƒ Xs â‰¢ âˆ… â†’ Exists (â‰¢ âˆ…) Xs.
+    Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.
 
     Context `{!LeibnizEquiv A}.
     Lemma non_empty_union_L X Y : X âˆª Y â‰  âˆ… â†’ X â‰  âˆ… âˆ¨ Y â‰  âˆ….
     Proof. unfold_leibniz. apply non_empty_union. Qed.
-    Lemma non_empty_list_union_L Xs : â‹ƒ Xs â‰  âˆ… â†’ Exists (â‰  âˆ…) Xs.
-    Proof. unfold_leibniz. apply non_empty_list_union. Qed.
+    Lemma non_empty_union_list_L Xs : â‹ƒ Xs â‰  âˆ… â†’ Exists (â‰  âˆ…) Xs.
+    Proof. unfold_leibniz. apply non_empty_union_list. Qed.
   End dec.
 End bounded_join_sl.
 
diff --git a/theories/pmap.v b/theories/pmap.v
index ee8d5550aee83f2eee2c32e539746e86a451f196..9b1ec6eb0c5c72ec79fcf7741a1f88054cd8d58f 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -69,7 +69,7 @@ thereby obtain a data type that ensures canonicity. *)
 Definition Pmap A := dsig (@Pmap_wf A).
 
 (** * Operations on the data structure *)
-Global Instance Pmap_dec `{âˆ€ x y : A, Decision (x = y)} (t1 t2 : Pmap A) :
+Global Instance Pmap_eq_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 (proj2 (dsig_eq _ t1 t2) H)
diff --git a/theories/tactics.v b/theories/tactics.v
index c55d57387359b0c4ffb28146c3b1d26d121d2e86..a16cb29377dfee4a3e60641cd1ab807799501636 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -55,14 +55,10 @@ Ltac case_match :=
   | |- context [ match ?x with _ => _ end ] => destruct x eqn:?
   end.
 
-(** The tactic [assert T unless tac_fail by tac_success] is used to assert
-[T] only if it is not provable by [tac_fail]. This is useful to build other
-tactics where only propositions that are not trivially provable are being
-asserted. *)
-Tactic Notation "assert" constr(T)
-    "unless" tactic3(tac_fail) "by" tactic3(tac_success)  := first
-  [ assert T by tac_fail; fail 1
-  | assert T by tac_success ].
+(** The tactic [unless T by tac_fail] succeeds if [T] is not provable by
+the tactic [tac_fail]. *)
+Tactic Notation "unless" constr(T) "by" tactic3(tac_fail) :=
+  first [assert T by tac_fail; fail 1 | idtac].
 
 (** The tactic [repeat_on_hyps tac] repeatedly applies [tac] in unspecified
 order on all hypotheses until it cannot be applied to any hypothesis anymore. *)
@@ -255,21 +251,33 @@ Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
   feed (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP) H.
 
 (** Coq's [firstorder] tactic fails or loops on rather small goals already. In 
-particular, on those generated by the tactic [unfold_elem_ofs] to solve
-propositions on collections. The [naive_solver] tactic implements an ad-hoc
-and incomplete [firstorder]-like solver using Ltac's backtracking mechanism.
-The tactic suffers from the following limitations:
+particular, on those generated by the tactic [unfold_elem_ofs] which is used
+to solve propositions on collections. The [naive_solver] tactic implements an
+ad-hoc and incomplete [firstorder]-like solver using Ltac's backtracking
+mechanism. The tactic suffers from the following limitations:
 - It might leave unresolved evars as Ltac provides no way to detect that.
-- To avoid the tactic going into pointless loops, it just does not allow a
-  universally quantified hypothesis to be used more than once.
+- To avoid the tactic becoming too slow, we allow a universally quantified
+  hypothesis to be instantiated only once during each search path.
 - It does not perform backtracking on instantiation of universally quantified
   assumptions.
 
+We use a counter to make the search breath first. Breath first search ensures
+that a minimal number of hypotheses is instantiated, and thus reduced the
+posibility that an evar remains unresolved.
+
 Despite these limitations, it works much better than Coq's [firstorder] tactic
 for the purposes of this development. This tactic either fails or proves the
 goal. *)
+Lemma forall_and_distr (A : Type) (P Q : A â†’ Prop) :
+  (âˆ€ x, P x âˆ§ Q x) â†” (âˆ€ x, P x) âˆ§ (âˆ€ x, Q x).
+Proof. firstorder. Qed.
+
 Tactic Notation "naive_solver" tactic(tac) :=
   unfold iff, not in *;
+  repeat match goal with
+  | H : context [âˆ€ _, _ âˆ§ _ ] |- _ =>
+     repeat setoid_rewrite forall_and_distr in H; revert H
+  end;
   let rec go n :=
   repeat match goal with
   (**i intros *)
@@ -278,52 +286,43 @@ Tactic Notation "naive_solver" tactic(tac) :=
   | H : False |- _ => destruct H
   | H : _ âˆ§ _ |- _ => destruct H
   | H : âˆƒ _, _  |- _ => destruct H
+  | H : ?P â†’ ?Q, H2 : ?Q |- _ => specialize (H H2)
   (**i simplify and solve equalities *)
   | |- _ => progress simpl in *
   | |- _ => progress simplify_equality
   (**i solve the goal *)
-  | |- _ => solve
-            [ eassumption
-            | symmetry; eassumption
-            | apply not_symmetry; eassumption
-            | reflexivity ]
+  | |- _ =>
+    solve
+    [ eassumption
+    | symmetry; eassumption
+    | apply not_symmetry; eassumption
+    | reflexivity ]
   (**i operations that generate more subgoals *)
   | |- _ âˆ§ _ => split
   | H : _ âˆ¨ _ |- _ => destruct H
   (**i solve the goal using the user supplied tactic *)
   | |- _ => solve [tac]
   end;
-  (**i use recursion to enable backtracking on the following clauses. We use
-  a counter to minimize the number of instantiations, and thus to reduce the
-  number of potentially unresolved meta variables. *)
-  first
-  [ iter (fun n' =>
-    match goal with 
-    (**i instantiations of assumptions *)
-    | H : _ â†’ _ |- _ =>
-      is_non_dependent H;
-      eapply H; clear H; go n'
-    | H : _ â†’ _ |- _ =>
-      is_non_dependent H;
-      (**i create subgoals for all premises *)
-      efeed H using (fun p =>
-        match type of p with
-        | _ âˆ§ _ =>
-          let H' := fresh in pose proof p as H'; destruct H'
-        | âˆƒ _, _ =>
-          let H' := fresh in pose proof p as H'; destruct H'
-        | _ âˆ¨ _ =>
-          let H' := fresh in pose proof p as H'; destruct H'
-        | False =>
-          let H' := fresh in pose proof p as H'; destruct H'
-        end) by (clear H; go n');
-      (**i solve these subgoals, but clear [H] to avoid loops *)
-      clear H; go n
-    end) (eval compute in (seq 0 n))
-  | match goal with
-    (**i instantiation of the conclusion *)
-    | |- âˆƒ x, _ => eexists; go n
-    | |- _ âˆ¨ _ => first [left; go n | right; go n]
-    end]
-  in go 10.
+  (**i use recursion to enable backtracking on the following clauses. *)
+  match goal with
+  (**i instantiation of the conclusion *)
+  | |- âˆƒ x, _ => eexists; go n
+  | |- _ âˆ¨ _ => first [left; go n | right; go n]
+  | _ =>
+    (**i instantiations of assumptions. *)
+    lazymatch n with
+    | S ?n' =>
+      (**i we give priority to assumptions that fit on the conclusion. *)
+      match goal with 
+      | H : _ â†’ _ |- _ =>
+        is_non_dependent H;
+        eapply H; clear H; go n'
+      | H : _ â†’ _ |- _ =>
+        is_non_dependent H;
+        try (eapply H; fail 2);
+        efeed pose proof H; clear H; go n'
+      end
+    end
+  end
+  in iter (fun n' => go n') (eval compute in (seq 0 6)).
 Tactic Notation "naive_solver" := naive_solver eauto.