diff --git a/_CoqProject b/_CoqProject
index 467bb6214aa4c5f0d5a4613b2f0ee85b7a43a335..11ce70ea254b642210ed772f7ce65cfce9152db5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -55,6 +55,7 @@ algebra/upred_tactics.v
 algebra/upred_big_op.v
 algebra/frac.v
 algebra/one_shot.v
+algebra/list.v
 program_logic/model.v
 program_logic/adequacy.v
 program_logic/hoare_lifting.v
diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 2e3d894e697aa8c1389696d05d14a7ad6e6cb12c..65f9f9256d7c8a4407c5d438ae768a685aff804f 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export cmra.
+From iris.algebra Require Export cmra list.
 From iris.prelude Require Import gmap.
 
 Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
@@ -25,8 +25,9 @@ Proof.
   - by rewrite !assoc (comm _ x).
   - by trans (big_op xs2).
 Qed.
-Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op.
+Global Instance big_op_ne n : Proper (dist n ==> dist n) big_op.
 Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
+Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op := ne_proper _.
 Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
 Proof.
   induction xs as [|x xs IH]; simpl; first by rewrite ?left_id.
@@ -64,7 +65,7 @@ Proof.
   { by intros m2; rewrite (symmetry_iff (≡)) map_equiv_empty; intros ->. }
   intros m2 Hm2; rewrite big_opM_insert //.
   rewrite (IH (delete i m2)); last by rewrite -Hm2 delete_insert.
-  destruct (map_equiv_lookup (<[i:=x]> m1) m2 i x)
+  destruct (map_equiv_lookup_l (<[i:=x]> m1) m2 i x)
     as (y&?&Hxy); auto using lookup_insert.
   rewrite Hxy -big_opM_insert; last auto using lookup_delete.
   by rewrite insert_delete.
diff --git a/algebra/list.v b/algebra/list.v
new file mode 100644
index 0000000000000000000000000000000000000000..6de96c2c0fbad24c0e415bfa277f9d9d22812d7e
--- /dev/null
+++ b/algebra/list.v
@@ -0,0 +1,108 @@
+From iris.algebra Require Export option.
+From iris.prelude Require Export list.
+
+Section cofe.
+Context {A : cofeT}.
+
+Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
+
+Global Instance cons_ne n : Proper (dist n ==> dist n ==> dist n) (@cons A) := _.
+Global Instance app_ne n : Proper (dist n ==> dist n ==> dist n) (@app A) := _.
+Global Instance length_ne n : Proper (dist n ==> (=)) (@length A) := _.
+Global Instance tail_ne n : Proper (dist n ==> dist n) (@tail A) := _.
+Global Instance take_ne n : Proper (dist n ==> dist n) (@take A n) := _.
+Global Instance drop_ne n : Proper (dist n ==> dist n) (@drop A n) := _.
+Global Instance list_lookup_ne n i :
+  Proper (dist n ==> dist n) (lookup (M:=list A) i).
+Proof. intros ???. by apply dist_option_Forall2, Forall2_lookup. Qed.
+Global Instance list_alter_ne n f i :
+  Proper (dist n ==> dist n) f →
+  Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
+Global Instance list_insert_ne n i :
+  Proper (dist n ==> dist n ==> dist n) (insert (M:=list A) i) := _.
+Global Instance list_inserts_ne n i :
+  Proper (dist n ==> dist n ==> dist n) (@list_inserts A i) := _.
+Global Instance list_delete_ne n i :
+  Proper (dist n ==> dist n) (delete (M:=list A) i) := _.
+Global Instance option_list_ne n : Proper (dist n ==> dist n) (@option_list A).
+Proof. intros ???; by apply Forall2_option_list, dist_option_Forall2. Qed.
+Global Instance list_filter_ne n P `{∀ x, Decision (P x)} :
+  Proper (dist n ==> iff) P →
+  Proper (dist n ==> dist n) (filter (B:=list A) P) := _.
+Global Instance replicate_ne n :
+  Proper (dist n ==> dist n) (@replicate A n) := _.
+Global Instance reverse_ne n : Proper (dist n ==> dist n) (@reverse A) := _.
+Global Instance last_ne n : Proper (dist n ==> dist n) (@last A).
+Proof. intros ???; by apply dist_option_Forall2, Forall2_last. Qed.
+Global Instance resize_ne n :
+  Proper (dist n ==> dist n ==> dist n) (@resize A n) := _.
+
+Program Definition list_chain
+    (c : chain (list A)) (x : A) (k : nat) : chain A :=
+  {| chain_car n := from_option x (c n !! k) |}.
+Next Obligation. intros c x k n i ?. by rewrite /= (chain_cauchy c n i). Qed.
+Instance list_compl : Compl (list A) := λ c,
+  match c 0 with
+  | [] => []
+  | x :: _ => compl ∘ list_chain c x <$> seq 0 (length (c 0))
+  end.
+
+Definition list_cofe_mixin : CofeMixin (list A).
+Proof.
+  split.
+  - intros l k. rewrite equiv_Forall2 -Forall2_forall.
+    split; induction 1; constructor; intros; try apply equiv_dist; auto.
+  - apply _.
+  - rewrite /dist /list_dist. eauto using Forall2_impl, dist_S.
+  - intros n c; rewrite /compl /list_compl.
+    destruct (c 0) as [|x l] eqn:Hc0 at 1.
+    { by destruct (chain_cauchy c 0 n); auto with omega. }
+    rewrite -(λ H, length_ne _ _ _ (chain_cauchy c 0 n H)); last omega.
+    apply Forall2_lookup=> i; apply dist_option_Forall2.
+    rewrite list_lookup_fmap. destruct (decide (i < length (c n))); last first.
+    { rewrite lookup_seq_ge ?lookup_ge_None_2; auto with omega. }
+    rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
+    by destruct (lookup_lt_is_Some_2 (c n) i) as [? ->].
+Qed.
+Canonical Structure listC := CofeT list_cofe_mixin.
+Global Instance list_discrete : Discrete A → Discrete listC.
+Proof. induction 2; constructor; try apply (timeless _); auto. Qed.
+
+Global Instance nil_timeless : Timeless (@nil A).
+Proof. inversion_clear 1; constructor. Qed.
+Global Instance cons_timeless x l : Timeless x → Timeless l → Timeless (x :: l).
+Proof. intros ??; inversion_clear 1; constructor; by apply timeless. Qed.
+End cofe.
+
+Arguments listC : clear implicits.
+
+(** Functor *)
+Instance list_fmap_ne {A B : cofeT} (f : A → B) n:
+  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=list) f).
+Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed. 
+Definition listC_map {A B} (f : A -n> B) : listC A -n> listC B :=
+  CofeMor (fmap f : listC A → listC B).
+Instance listC_map_ne A B n : Proper (dist n ==> dist n) (@listC_map A B).
+Proof. intros f f' ? l; by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
+
+Program Definition listCF (F : cFunctor) : cFunctor := {|
+  cFunctor_car A B := listC (cFunctor_car F A B);
+  cFunctor_map A1 A2 B1 B2 fg := listC_map (cFunctor_map F fg)
+|}.
+Next Obligation.
+  by intros F A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, cFunctor_ne.
+Qed.
+Next Obligation.
+  intros F A B x. rewrite /= -{2}(list_fmap_id x).
+  apply list_fmap_setoid_ext=>y. apply cFunctor_id.
+Qed.
+Next Obligation.
+  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
+  apply list_fmap_setoid_ext=>y; apply cFunctor_compose.
+Qed.
+
+Instance listCF_contractive F :
+  cFunctorContractive F → cFunctorContractive (listCF F).
+Proof.
+  by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, cFunctor_contractive.
+Qed.
diff --git a/algebra/option.v b/algebra/option.v
index 1a34c48279e2ec41d5f11c0ff2c43d5a6c7a85e8..86007543ad3f1fcac064457d50d3c7e6f73c784b 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -4,40 +4,50 @@ From iris.algebra Require Import upred.
 (* COFE *)
 Section cofe.
 Context {A : cofeT}.
-Inductive option_dist : Dist (option A) :=
-  | Some_dist n x y : x ≡{n}≡ y → Some x ≡{n}≡ Some y
-  | None_dist n : None ≡{n}≡ None.
-Existing Instance option_dist.
+
+Inductive option_dist' (n : nat) : relation (option A) :=
+  | Some_dist x y : x ≡{n}≡ y → option_dist' n (Some x) (Some y)
+  | None_dist : option_dist' n None None.
+Instance option_dist : Dist (option A) := option_dist'.
+
+Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
+Proof. split; destruct 1; constructor; auto. Qed.
+
 Program Definition option_chain (c : chain (option A)) (x : A) : chain A :=
   {| chain_car n := from_option x (c n) |}.
 Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
 Instance option_compl : Compl (option A) := λ c,
   match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
+
 Definition option_cofe_mixin : CofeMixin (option A).
 Proof.
   split.
   - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
-    intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
+    intros Hxy; destruct (Hxy 0); constructor; apply equiv_dist.
     by intros n; feed inversion (Hxy n).
   - intros n; split.
     + by intros [x|]; constructor.
     + by destruct 1; constructor.
     + destruct 1; inversion_clear 1; constructor; etrans; eauto.
-  - by inversion_clear 1; constructor; apply dist_S.
+  - destruct 1; constructor; by apply dist_S.
   - intros n c; rewrite /compl /option_compl.
     feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
     rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver.
 Qed.
 Canonical Structure optionC := CofeT option_cofe_mixin.
 Global Instance option_discrete : Discrete A → Discrete optionC.
-Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.
+Proof. destruct 2; constructor; by apply (timeless _). Qed.
 
 Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
 Proof. by constructor. Qed.
 Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
-Proof. inversion_clear 1; split; eauto. Qed.
+Proof. destruct 1; split; eauto. Qed.
 Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
 Proof. by inversion_clear 1. Qed.
+Global Instance from_option_ne n :
+  Proper (dist n ==> dist n ==> dist n) (@from_option A).
+Proof. by destruct 2. Qed.
+
 Global Instance None_timeless : Timeless (@None A).
 Proof. inversion_clear 1; constructor. Qed.
 Global Instance Some_timeless x : Timeless x → Timeless (Some x).
@@ -125,16 +135,16 @@ Global Instance option_persistent (mx : option A) :
 Proof. intros. destruct mx. apply _. apply cmra_unit_persistent. Qed.
 
 (** Internalized properties *)
-Lemma option_equivI {M} (x y : option A) :
-  (x ≡ y) ⊣⊢ (match x, y with
-               | Some a, Some b => a ≡ b | None, None => True | _, _ => False
-               end : uPred M).
+Lemma option_equivI {M} (mx my : option A) :
+  (mx ≡ my) ⊣⊢ (match mx, my with
+                | Some x, Some y => x ≡ y | None, None => True | _, _ => False
+                end : uPred M).
 Proof.
-  uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
+  uPred.unseal. do 2 split. by destruct 1. by destruct mx, my; try constructor.
 Qed.
-Lemma option_validI {M} (x : option A) :
-  (✓ x) ⊣⊢ (match x with Some a => ✓ a | None => True end : uPred M).
-Proof. uPred.unseal. by destruct x. Qed.
+Lemma option_validI {M} (mx : option A) :
+  (✓ mx) ⊣⊢ (match mx with Some x => ✓ x | None => True end : uPred M).
+Proof. uPred.unseal. by destruct mx. Qed.
 
 (** Updates *)
 Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
@@ -146,7 +156,7 @@ Proof.
   by exists (Some y'); split; [auto|apply cmra_validN_op_l with (core x)].
 Qed.
 Lemma option_updateP' (P : A → Prop) x :
-  x ~~>: P → Some x ~~>: λ y, default False y P.
+  x ~~>: P → Some x ~~>: λ my, default False my P.
 Proof. eauto using option_updateP. Qed.
 Lemma option_update x y : x ~~> y → Some x ~~> Some y.
 Proof.
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index d82f64ac88494fc092d229ffd1cf0ca848ff69eb..fe35a51e6d93ee631b01471bdbac8abac5129aff 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export upred.
+From iris.algebra Require Export upred list.
 From iris.prelude Require Import gmap fin_collections.
 Import uPred.
 
@@ -44,11 +44,9 @@ Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 Global Instance big_sep_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_sep M).
 Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
-Global Instance big_and_ne n :
-  Proper (Forall2 (dist n) ==> dist n) (@uPred_big_and M).
+Global Instance big_and_ne n : Proper (dist n ==> dist n) (@uPred_big_and M).
 Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-Global Instance big_sep_ne n :
-  Proper (Forall2 (dist n) ==> dist n) (@uPred_big_sep M).
+Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M).
 Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
 Global Instance big_and_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_and M).
@@ -71,26 +69,26 @@ Proof.
   - etrans; eauto.
 Qed.
 
-Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs)) ⊣⊢ (Π∧ Ps ∧ Π∧ Qs).
+Lemma big_and_app Ps Qs : Π∧ (Ps ++ Qs) ⊣⊢ (Π∧ Ps ∧ Π∧ Qs).
 Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
-Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs)) ⊣⊢ (Π★ Ps ★ Π★ Qs).
+Lemma big_sep_app Ps Qs : Π★ (Ps ++ Qs) ⊣⊢ (Π★ Ps ★ Π★ Qs).
 Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
 
-Lemma big_and_contains Ps Qs : Qs `contains` Ps → (Π∧ Ps) ⊢ (Π∧ Qs).
+Lemma big_and_contains Ps Qs : Qs `contains` Ps → Π∧ Ps ⊢ Π∧ Qs.
 Proof.
   intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
 Qed.
-Lemma big_sep_contains Ps Qs : Qs `contains` Ps → (Π★ Ps) ⊢ (Π★ Qs).
+Lemma big_sep_contains Ps Qs : Qs `contains` Ps → Π★ Ps ⊢ Π★ Qs.
 Proof.
   intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
 Qed.
 
-Lemma big_sep_and Ps : (Π★ Ps) ⊢ (Π∧ Ps).
+Lemma big_sep_and Ps : Π★ Ps ⊢ Π∧ Ps.
 Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
 
-Lemma big_and_elem_of Ps P : P ∈ Ps → (Π∧ Ps) ⊢ P.
+Lemma big_and_elem_of Ps P : P ∈ Ps → Π∧ Ps ⊢ P.
 Proof. induction 1; simpl; auto with I. Qed.
-Lemma big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊢ P.
+Lemma big_sep_elem_of Ps P : P ∈ Ps → Π★ Ps ⊢ P.
 Proof. induction 1; simpl; auto with I. Qed.
 
 (* Big ops over finite maps *)
@@ -101,11 +99,11 @@ Section gmap.
 
   Lemma big_sepM_mono Φ Ψ m1 m2 :
     m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → Φ k x ⊢ Ψ k x) →
-    (Π★{map m1} Φ) ⊢ (Π★{map m2} Ψ).
+    Π★{map m1} Φ ⊢ Π★{map m2} Ψ.
   Proof.
     intros HX HΦ. trans (Π★{map m2} Φ)%I.
     - by apply big_sep_contains, fmap_contains, map_to_list_contains.
-    - apply big_sep_mono', Forall2_fmap, Forall2_Forall.
+    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
       apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
   Qed.
 
@@ -114,7 +112,7 @@ Section gmap.
            (uPred_big_sepM (M:=M) m).
   Proof.
     intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
-    apply Forall2_Forall, Forall_true=> -[i x]; apply HΦ.
+    apply Forall_Forall2, Forall_true=> -[i x]; apply HΦ.
   Qed.
   Global Instance big_sepM_proper m :
     Proper (pointwise_relation _ (pointwise_relation _ (⊣⊢)) ==> (⊣⊢))
@@ -128,25 +126,25 @@ Section gmap.
            (uPred_big_sepM (M:=M) m).
   Proof. intros Φ1 Φ2 HΦ. apply big_sepM_mono; intros; [done|apply HΦ]. Qed.
 
-  Lemma big_sepM_empty Φ : (Π★{map ∅} Φ) ⊣⊢ True.
+  Lemma big_sepM_empty Φ : Π★{map ∅} Φ ⊣⊢ True.
   Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
   Lemma big_sepM_insert Φ (m : gmap K A) i x :
-    m !! i = None → (Π★{map <[i:=x]> m} Φ) ⊣⊢ (Φ i x ★ Π★{map m} Φ).
+    m !! i = None → Π★{map <[i:=x]> m} Φ ⊣⊢ (Φ i x ★ Π★{map m} Φ).
   Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
-  Lemma big_sepM_singleton Φ i x : (Π★{map {[i := x]}} Φ) ⊣⊢ (Φ i x).
+  Lemma big_sepM_singleton Φ i x : Π★{map {[i := x]}} Φ ⊣⊢ (Φ i x).
   Proof.
     rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
     by rewrite big_sepM_empty right_id.
   Qed.
 
   Lemma big_sepM_sepM Φ Ψ m :
-    (Π★{map m} (λ i x, Φ i x ★ Ψ i x)) ⊣⊢ (Π★{map m} Φ ★ Π★{map m} Ψ).
+    Π★{map m} (λ i x, Φ i x ★ Ψ i x) ⊣⊢ (Π★{map m} Φ ★ Π★{map m} Ψ).
   Proof.
     rewrite /uPred_big_sepM.
     induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
     by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc.
   Qed.
-  Lemma big_sepM_later Φ m : (▷ Π★{map m} Φ) ⊣⊢ (Π★{map m} (λ i x, ▷ Φ i x)).
+  Lemma big_sepM_later Φ m : ▷ Π★{map m} Φ ⊣⊢ Π★{map m} (λ i x, ▷ Φ i x).
   Proof.
     rewrite /uPred_big_sepM.
     induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
@@ -161,11 +159,11 @@ Section gset.
   Implicit Types Φ : A → uPred M.
 
   Lemma big_sepS_mono Φ Ψ X Y :
-    Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → (Π★{set X} Φ) ⊢ (Π★{set Y} Ψ).
+    Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → Π★{set X} Φ ⊢ Π★{set Y} Ψ.
   Proof.
     intros HX HΦ. trans (Π★{set Y} Φ)%I.
     - by apply big_sep_contains, fmap_contains, elements_contains.
-    - apply big_sep_mono', Forall2_fmap, Forall2_Forall.
+    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
       apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
   Qed.
 
@@ -173,7 +171,7 @@ Section gset.
     Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
   Proof.
     intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
-    apply Forall2_Forall, Forall_true=> x; apply HΦ.
+    apply Forall_Forall2, Forall_true=> x; apply HΦ.
   Qed.
   Lemma big_sepS_proper X :
     Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (uPred_big_sepS (M:=M) X).
@@ -185,29 +183,29 @@ Section gset.
     Proper (pointwise_relation _ (⊢) ==> (⊢)) (uPred_big_sepS (M:=M) X).
   Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
 
-  Lemma big_sepS_empty Φ : (Π★{set ∅} Φ) ⊣⊢ True.
+  Lemma big_sepS_empty Φ : Π★{set ∅} Φ ⊣⊢ True.
   Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
   Lemma big_sepS_insert Φ X x :
-    x ∉ X → (Π★{set {[ x ]} ∪ X} Φ) ⊣⊢ (Φ x ★ Π★{set X} Φ).
+    x ∉ X → Π★{set {[ x ]} ∪ X} Φ ⊣⊢ (Φ x ★ Π★{set X} Φ).
   Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
   Lemma big_sepS_delete Φ X x :
-    x ∈ X → (Π★{set X} Φ) ⊣⊢ (Φ x ★ Π★{set X ∖ {[ x ]}} Φ).
+    x ∈ X → Π★{set X} Φ ⊣⊢ (Φ x ★ Π★{set X ∖ {[ x ]}} Φ).
   Proof.
     intros. rewrite -big_sepS_insert; last set_solver.
     by rewrite -union_difference_L; last set_solver.
   Qed.
-  Lemma big_sepS_singleton Φ x : (Π★{set {[ x ]}} Φ) ⊣⊢ (Φ x).
+  Lemma big_sepS_singleton Φ x : Π★{set {[ x ]}} Φ ⊣⊢ (Φ x).
   Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
 
   Lemma big_sepS_sepS Φ Ψ X :
-    (Π★{set X} (λ x, Φ x ★ Ψ x)) ⊣⊢ (Π★{set X} Φ ★ Π★{set X} Ψ).
+    Π★{set X} (λ x, Φ x ★ Ψ x) ⊣⊢ (Π★{set X} Φ ★ Π★{set X} Ψ).
   Proof.
     rewrite /uPred_big_sepS.
     induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
     by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc.
   Qed.
 
-  Lemma big_sepS_later Φ X : (▷ Π★{set X} Φ) ⊣⊢ (Π★{set X} (λ x, ▷ Φ x)).
+  Lemma big_sepS_later Φ X : ▷ Π★{set X} Φ ⊣⊢ Π★{set X} (λ x, ▷ Φ x).
   Proof.
     rewrite /uPred_big_sepS.
     induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index ba5dab026a0685ece29b81b7af48c8ff48347f3b..ac03c01b3c0112a7e5f1535c165323af2dfd813b 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -173,11 +173,9 @@ Section setoid.
     split; [intros Hm; apply map_eq; intros i|by intros ->].
     by rewrite lookup_empty, <-equiv_None, Hm, lookup_empty.
   Qed.
-  Lemma map_equiv_lookup (m1 m2 : M A) i x :
+  Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
     m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y.
-  Proof.
-    intros Hm ?. destruct (equiv_Some (m1 !! i) (m2 !! i) x) as (y&?&?); eauto.
-  Qed.
+  Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.
 End setoid.
 
 (** ** General properties *)
diff --git a/prelude/list.v b/prelude/list.v
index ef4d127b569951e33b5d30d151c00569a56ef8ad..84cea61d05254944f219d9920cc2b031bbfe76f7 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -8,16 +8,26 @@ From iris.prelude Require Export numbers base option.
 Arguments length {_} _.
 Arguments cons {_} _ _.
 Arguments app {_} _ _.
-Arguments Permutation {_} _ _.
-Arguments Forall_cons {_} _ _ _ _ _.
+
+Instance: Params (@length) 1.
+Instance: Params (@cons) 1.
+Instance: Params (@app) 1.
 
 Notation tail := tl.
 Notation take := firstn.
 Notation drop := skipn.
 
+Arguments tail {_} _.
 Arguments take {_} !_ !_ /.
 Arguments drop {_} !_ !_ /.
 
+Instance: Params (@tail) 1.
+Instance: Params (@take) 1.
+Instance: Params (@drop) 1.
+
+Arguments Permutation {_} _ _.
+Arguments Forall_cons {_} _ _ _ _ _.
+
 Notation "(::)" := cons (only parsing) : C_scope.
 Notation "( x ::)" := (cons x) (only parsing) : C_scope.
 Notation "(:: l )" := (λ x, cons x l) (only parsing) : C_scope.
@@ -74,6 +84,7 @@ Fixpoint list_inserts {A} (i : nat) (k l : list A) : list A :=
   | [] => l
   | y :: k => <[i:=y]>(list_inserts (S i) k l)
   end.
+Instance: Params (@list_inserts) 1.
 
 (** 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,
@@ -88,7 +99,8 @@ Instance list_delete {A} : Delete nat (list A) :=
 (** 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]) [].
-Definition list_singleton {A} (l : list A) : option A :=
+Instance: Params (@option_list) 1.
+Instance maybe_list_singleton {A} : Maybe (λ x : A, [x]) := λ l,
   match l with [x] => Some x | _ => None end.
 
 (** The function [filter P l] returns the list of elements of [l] that
@@ -108,19 +120,23 @@ Definition list_find {A} P `{∀ x, Decision (P x)} : list A → option (nat * A
   | [] => None
   | x :: l => if decide (P x) then Some (0,x) else prod_map S id <$> go l
   end.
+Instance: Params (@list_find) 3.
 
 (** The function [replicate n x] generates a list with length [n] of elements
 with value [x]. *)
 Fixpoint replicate {A} (n : nat) (x : A) : list A :=
   match n with 0 => [] | S n => x :: replicate n x end.
+Instance: Params (@replicate) 2.
 
 (** The function [reverse l] returns the elements of [l] in reverse order. *)
 Definition reverse {A} (l : list A) : list A := rev_append l [].
+Instance: Params (@reverse) 1.
 
 (** The function [last l] returns the last element of the list [l], or [None]
 if the list [l] is empty. *)
 Fixpoint last {A} (l : list A) : option A :=
   match l with [] => None | [x] => Some x | _ :: l => last l end.
+Instance: Params (@last) 1.
 
 (** The function [resize n y l] takes the first [n] elements of [l] in case
 [length l ≤ n], and otherwise appends elements with value [x] to [l] to obtain
@@ -131,6 +147,7 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
   | x :: l => match n with 0 => [] | S n => x :: resize n y l end
   end.
 Arguments resize {_} !_ _ !_.
+Instance: Params (@resize) 2.
 
 (** The function [reshape k l] transforms [l] into a list of lists whose sizes
 are specified by [k]. In case [l] is too short, the resulting list will be
@@ -139,6 +156,7 @@ Fixpoint reshape {A} (szs : list nat) (l : list A) : list (list A) :=
   match szs with
   | [] => [] | sz :: szs => take sz l :: reshape szs (drop sz l)
   end.
+Instance: Params (@reshape) 2.
 
 Definition sublist_lookup {A} (i n : nat) (l : list A) : option (list A) :=
   guard (i + n ≤ length l); Some (take n (drop i l)).
@@ -366,27 +384,6 @@ Context {A : Type}.
 Implicit Types x y z : A.
 Implicit Types l k : list A.
 
-Section setoid.
-  Context `{Equiv A} `{!Equivalence ((≡) : relation A)}.
-  Global Instance map_equivalence : Equivalence ((≡) : relation (list A)).
-  Proof.
-    split.
-    - intros l; induction l; constructor; auto.
-    - induction 1; constructor; auto.
-    - intros l1 l2 l3 Hl; revert l3.
-      induction Hl; inversion_clear 1; constructor; try etrans; eauto.
-  Qed.
-  Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A).
-  Proof. by constructor. Qed.
-  Global Instance app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@app A).
-  Proof.
-    induction 1 as [|x y l k ?? IH]; intros ?? Htl; simpl; auto.
-    by apply cons_equiv, IH.
-  Qed.
-  Global Instance list_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (list A).
-  Proof. induction 1; f_equal; fold_leibniz; auto. Qed.
-End setoid.
-
 Global Instance: Inj2 (=) (=) (=) (@cons A).
 Proof. by injection 1. Qed.
 Global Instance: ∀ k, Inj (=) (=) (k ++).
@@ -409,18 +406,18 @@ Lemma cons_middle x l1 l2 : l1 ++ x :: l2 = l1 ++ [x] ++ l2.
 Proof. done. Qed.
 Lemma list_eq l1 l2 : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
 Proof.
-  revert l2. induction l1; intros [|??] H.
+  revert l2. induction l1 as [|x l1 IH]; intros [|y l2] H.
   - done.
   - discriminate (H 0).
   - discriminate (H 0).
-  - f_equal; [by injection (H 0)|]. apply (IHl1 _ $ λ i, H (S i)).
+  - f_equal; [by injection (H 0)|]. apply (IH _ $ λ i, H (S i)).
 Qed.
 Global Instance list_eq_dec {dec : ∀ x y, Decision (x = y)} : ∀ l k,
   Decision (l = k) := list_eq_dec dec.
 Global Instance list_eq_nil_dec l : Decision (l = []).
 Proof. by refine match l with [] => left _ | _ => right _ end. Defined.
 Lemma list_singleton_reflect l :
-  option_reflect (λ x, l = [x]) (length l ≠ 1) (list_singleton l).
+  option_reflect (λ x, l = [x]) (length l ≠ 1) (maybe (λ x, [x]) l).
 Proof. by destruct l as [|? []]; constructor. Defined.
 
 Definition nil_length : length (@nil A) = 0 := eq_refl.
@@ -434,15 +431,11 @@ Proof. by destruct i. Qed.
 Lemma lookup_tail l i : tail l !! i = l !! S i.
 Proof. by destruct l. Qed.
 Lemma lookup_lt_Some l i x : l !! i = Some x → i < length l.
-Proof.
-  revert i. induction l; intros [|?] ?; simplify_eq/=; auto with arith.
-Qed.
+Proof. revert i. induction l; intros [|?] ?; naive_solver auto with arith. Qed.
 Lemma lookup_lt_is_Some_1 l i : is_Some (l !! i) → i < length l.
 Proof. intros [??]; eauto using lookup_lt_Some. Qed.
 Lemma lookup_lt_is_Some_2 l i : i < length l → is_Some (l !! i).
-Proof.
-  revert i. induction l; intros [|?] ?; simplify_eq/=; eauto with lia.
-Qed.
+Proof. revert i. induction l; intros [|?] ?; naive_solver eauto with lia. Qed.
 Lemma lookup_lt_is_Some l i : is_Some (l !! i) ↔ i < length l.
 Proof. split; auto using lookup_lt_is_Some_1, lookup_lt_is_Some_2. Qed.
 Lemma lookup_ge_None l i : l !! i = None ↔ length l ≤ i.
@@ -462,7 +455,7 @@ Proof.
   - by rewrite lookup_ge_None, Hlen, <-lookup_ge_None.
 Qed.
 Lemma lookup_app_l l1 l2 i : i < length l1 → (l1 ++ l2) !! i = l1 !! i.
-Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
+Proof. revert i. induction l1; intros [|?]; naive_solver auto with lia. Qed.
 Lemma lookup_app_l_Some l1 l2 i x : l1 !! i = Some x → (l1 ++ l2) !! i = Some x.
 Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_Some. Qed.
 Lemma lookup_app_r l1 l2 i :
@@ -491,15 +484,11 @@ Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
 Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
 Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
 Lemma list_lookup_alter_ne f l i j : i ≠ j → alter f i l !! j = l !! j.
-Proof.
-  revert i j. induction l; [done|]. intros [][] ?; csimpl; auto with congruence.
-Qed.
+Proof. revert i j. induction l; [done|]. intros [] []; naive_solver. Qed.
 Lemma list_lookup_insert l i x : i < length l → <[i:=x]>l !! i = Some x.
 Proof. revert i. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
 Lemma list_lookup_insert_ne l i j x : i ≠ j → <[i:=x]>l !! j = l !! j.
-Proof.
-  revert i j. induction l; [done|]. intros [] [] ?; simpl; auto with congruence.
-Qed.
+Proof. revert i j. induction l; [done|]. intros [] []; naive_solver. Qed.
 Lemma list_lookup_insert_Some l i x j y :
   <[i:=x]>l !! j = Some y ↔
     i = j ∧ x = y ∧ j < length l ∨ i ≠ j ∧ l !! j = Some y.
@@ -814,9 +803,9 @@ Section find.
   Lemma list_find_Some l i x :
     list_find P l = Some (i,x) → l !! i = Some x ∧ P x.
   Proof.
-    revert i; induction l; intros [] ?;
-      repeat (match goal with x : prod _ _ |- _ => destruct x end
-              || simplify_option_eq); eauto.
+    revert i; induction l; intros [] ?; repeat first
+      [ match goal with x : prod _ _ |- _ => destruct x end
+      | simplify_option_eq ]; eauto.
   Qed.
   Lemma list_find_elem_of l x : x ∈ l → P x → is_Some (list_find P l).
   Proof.
@@ -1131,12 +1120,6 @@ Proof.
 Qed.
 Lemma lookup_resize_old l n x i : n ≤ i → resize n x l !! i = None.
 Proof. intros ?. apply lookup_ge_None_2. by rewrite resize_length. Qed.
-End general_properties.
-
-Section more_general_properties.
-Context {A : Type}.
-Implicit Types x y z : A.
-Implicit Types l k : list A.
 
 (** ** Properties of the [reshape] function *)
 Lemma reshape_length szs l : length (reshape szs l) = length szs.
@@ -1149,6 +1132,12 @@ Proof.
 Qed.
 Lemma sum_list_replicate n m : sum_list (replicate m n) = m * n.
 Proof. induction m; simpl; auto. Qed.
+End general_properties.
+
+Section more_general_properties.
+Context {A : Type}.
+Implicit Types x y z : A.
+Implicit Types l k : list A.
 
 (** ** Properties of [sublist_lookup] and [sublist_alter] *)
 Lemma sublist_lookup_length l i n k :
@@ -2026,10 +2015,9 @@ Global Instance included_preorder : PreOrder (@included A).
 Proof. split; firstorder. Qed.
 Lemma included_nil l : [] `included` l.
 Proof. intros x. by rewrite elem_of_nil. Qed.
-End more_general_properties.
 
 (** ** Properties of the [Forall] and [Exists] predicate *)
-Lemma Forall_Exists_dec {A} {P Q : A → Prop} (dec : ∀ x, {P x} + {Q x}) :
+Lemma Forall_Exists_dec {P Q : A → Prop} (dec : ∀ x, {P x} + {Q x}) :
   ∀ l, {Forall P l} + {Exists Q l}.
 Proof.
  refine (
@@ -2041,7 +2029,7 @@ Proof.
 Defined.
 
 Section Forall_Exists.
-  Context {A} (P : A → Prop).
+  Context (P : A → Prop).
 
   Definition Forall_nil_2 := @Forall_nil A.
   Definition Forall_cons_2 := @Forall_cons A.
@@ -2225,12 +2213,13 @@ Section Forall_Exists.
     end.
 End Forall_Exists.
 
-Lemma replicate_as_Forall {A} (x : A) n l :
+Lemma replicate_as_Forall (x : A) n l :
   replicate n x = l ↔ length l = n ∧ Forall (x =) l.
 Proof. rewrite replicate_as_elem_of, Forall_forall. naive_solver. Qed.
-Lemma replicate_as_Forall_2 {A} (x : A) n l :
+Lemma replicate_as_Forall_2 (x : A) n l :
   length l = n → Forall (x =) l → replicate n x = l.
 Proof. by rewrite replicate_as_Forall. Qed.
+End more_general_properties.
 
 Lemma Forall_swap {A B} (Q : A → B → Prop) l1 l2 :
   Forall (λ y, Forall (Q y) l1) l2 ↔ Forall (λ x, Forall (flip Q x) l2) l1.
@@ -2253,11 +2242,6 @@ Section Forall2.
   Implicit Types l : list A.
   Implicit Types k : list B.
 
-  Lemma Forall2_true l k :
-    (∀ x y, P x y) → length l = length k → Forall2 P l k.
-  Proof.
-    intro. revert k. induction l; intros [|??] ?; simplify_eq/=; auto.
-  Qed.
   Lemma Forall2_same_length l k :
     Forall2 (λ _ _, True) l k ↔ length l = length k.
   Proof.
@@ -2270,10 +2254,48 @@ Section Forall2.
   Proof. intros ? <-; symmetry. by apply Forall2_length. Qed.
   Lemma Forall2_length_r l k n : Forall2 P l k → length k = n → length l = n.
   Proof. intros ? <-. by apply Forall2_length. Qed.
+
+  Lemma Forall2_true l k : (∀ x y, P x y) → length l = length k → Forall2 P l k.
+  Proof. rewrite <-Forall2_same_length. induction 2; naive_solver. Qed.
+  Lemma Forall2_flip l k : Forall2 (flip P) k l ↔ Forall2 P l k.
+  Proof. split; induction 1; constructor; auto. Qed.
+  Lemma Forall2_transitive {C} (Q : B → C → Prop) (R : A → C → Prop) l k lC :
+    (∀ x y z, P x y → Q y z → R x z) →
+    Forall2 P l k → Forall2 Q k lC → Forall2 R l lC.
+  Proof. intros ? Hl. revert lC. induction Hl; inversion_clear 1; eauto. Qed.
+  Lemma Forall2_impl (Q : A → B → Prop) l k :
+    Forall2 P l k → (∀ x y, P x y → Q x y) → Forall2 Q l k.
+  Proof. intros H ?. induction H; auto. Defined.
+  Lemma Forall2_unique l k1 k2 :
+    Forall2 P l k1 → Forall2 P l k2 →
+    (∀ x y1 y2, P x y1 → P x y2 → y1 = y2) → k1 = k2.
+  Proof.
+    intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto.
+  Qed.
+  Lemma Forall2_forall `{Inhabited C} (Q : C → A → B → Prop) l k :
+    Forall2 (λ x y, ∀ z, Q z x y) l k ↔ ∀ z, Forall2 (Q z) l k.
+  Proof.
+    split; [induction 1; constructor; auto|].
+    intros Hlk. induction (Hlk inhabitant) as [|x y l k _ _ IH]; constructor.
+    - intros z. by feed inversion (Hlk z).
+    - apply IH. intros z. by feed inversion (Hlk z).
+  Qed.
+
+  Lemma Forall_Forall2 (Q : A → A → Prop) l :
+    Forall (λ x, Q x x) l → Forall2 Q l l.
+  Proof. induction 1; constructor; auto. Qed.
+  Lemma Forall2_Forall_l (Q : A → Prop) l k :
+    Forall2 P l k → Forall (λ y, ∀ x, P x y → Q x) k → Forall Q l.
+  Proof. induction 1; inversion_clear 1; eauto. Qed.
+  Lemma Forall2_Forall_r (Q : B → Prop) l k :
+    Forall2 P l k → Forall (λ x, ∀ y, P x y → Q y) l → Forall Q k.
+  Proof. induction 1; inversion_clear 1; eauto. Qed.
+
   Lemma Forall2_nil_inv_l k : Forall2 P [] k → k = [].
   Proof. by inversion 1. Qed.
   Lemma Forall2_nil_inv_r l : Forall2 P l [] → l = [].
   Proof. by inversion 1. Qed.
+
   Lemma Forall2_cons_inv x l y k :
     Forall2 P (x :: l) (y :: k) → P x y ∧ Forall2 P l k.
   Proof. by inversion 1. Qed.
@@ -2287,6 +2309,7 @@ Section Forall2.
   Proof. by inversion 1. Qed.
   Lemma Forall2_nil_cons_inv y k : Forall2 P [] (y :: k) → False.
   Proof. by inversion 1. Qed.
+
   Lemma Forall2_app_l l1 l2 k :
     Forall2 P l1 (take (length l1) k) → Forall2 P l2 (drop (length l1) k) →
     Forall2 P (l1 ++ l2) k.
@@ -2315,39 +2338,34 @@ Section Forall2.
     split; [|intros (?&?&?&?&->); by apply Forall2_app].
     revert l. induction k1; inversion 1; naive_solver.
   Qed.
-  Lemma Forall2_flip l k : Forall2 (flip P) k l ↔ Forall2 P l k.
-  Proof. split; induction 1; constructor; auto. Qed.
-  Lemma Forall2_impl (Q : A → B → Prop) l k :
-    Forall2 P l k → (∀ x y, P x y → Q x y) → Forall2 Q l k.
-  Proof. intros H ?. induction H; auto. Defined.
-  Lemma Forall2_unique l k1 k2 :
-    Forall2 P l k1 →  Forall2 P l k2 →
-    (∀ x y1 y2, P x y1 → P x y2 → y1 = y2) → k1 = k2.
+
+  Lemma Forall2_tail l k : Forall2 P l k → Forall2 P (tail l) (tail k).
+  Proof. destruct 1; simpl; auto. Qed.
+  Lemma Forall2_take l k n : Forall2 P l k → Forall2 P (take n l) (take n k).
+  Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
+  Lemma Forall2_drop l k n : Forall2 P l k → Forall2 P (drop n l) (drop n k).
+  Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
+
+  Lemma Forall2_lookup l k :
+    Forall2 P l k ↔ ∀ i, option_Forall2 P (l !! i) (k !! i).
   Proof.
-    intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto.
+    split; [induction 1; intros [|?]; simpl; try constructor; eauto|].
+    revert k. induction l as [|x l IH]; intros [| y k] H.
+    - done.
+    - feed inversion (H 0).
+    - feed inversion (H 0).
+    - constructor; [by feed inversion (H 0)|]. apply (IH _ $ λ i, H (S i)).
   Qed.
-  Lemma Forall2_Forall_l (Q : A → Prop) l k :
-    Forall2 P l k → Forall (λ y, ∀ x, P x y → Q x) k → Forall Q l.
-  Proof. induction 1; inversion_clear 1; eauto. Qed.
-  Lemma Forall2_Forall_r (Q : B → Prop) l k :
-    Forall2 P l k → Forall (λ x, ∀ y, P x y → Q y) l → Forall Q k.
-  Proof. induction 1; inversion_clear 1; eauto. Qed.
   Lemma Forall2_lookup_lr l k i x y :
     Forall2 P l k → l !! i = Some x → k !! i = Some y → P x y.
-  Proof.
-    intros H. revert i. induction H; intros [|?] ??; simplify_eq/=; eauto.
-  Qed.
+  Proof. rewrite Forall2_lookup; intros H; destruct (H i); naive_solver. Qed.
   Lemma Forall2_lookup_l l k i x :
     Forall2 P l k → l !! i = Some x → ∃ y, k !! i = Some y ∧ P x y.
-  Proof.
-    intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
-  Qed.
+  Proof. rewrite Forall2_lookup; intros H; destruct (H i); naive_solver. Qed.
   Lemma Forall2_lookup_r l k i y :
     Forall2 P l k → k !! i = Some y → ∃ x, l !! i = Some x ∧ P x y.
-  Proof.
-    intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
-  Qed.
-  Lemma Forall2_lookup_2 l k :
+  Proof. rewrite Forall2_lookup; intros H; destruct (H i); naive_solver. Qed.
+  Lemma Forall2_same_length_lookup_2 l k :
     length l = length k →
     (∀ i x y, l !! i = Some x → k !! i = Some y → P x y) → Forall2 P l k.
   Proof.
@@ -2355,14 +2373,15 @@ Section Forall2.
     induction Hl as [|?????? IH]; constructor; [by apply (Hlookup 0)|].
     apply IH. apply (λ i, Hlookup (S i)).
   Qed.
-  Lemma Forall2_lookup l k :
-    Forall2 P l k ↔ length l = length k ∧
+  Lemma Forall2_same_length_lookup l k :
+    Forall2 P l k ↔
+      length l = length k ∧
       (∀ i x y, l !! i = Some x → k !! i = Some y → P x y).
   Proof.
-    naive_solver eauto using Forall2_length, Forall2_lookup_lr,Forall2_lookup_2.
+    naive_solver eauto using Forall2_length,
+      Forall2_lookup_lr, Forall2_same_length_lookup_2.
   Qed.
-  Lemma Forall2_tail l k : Forall2 P l k → Forall2 P (tail l) (tail k).
-  Proof. destruct 1; simpl; auto. Qed.
+
   Lemma Forall2_alter_l f l k i :
     Forall2 P l k →
     (∀ x y, l !! i = Some x → k !! i = Some y → P x y → P (f x) y) →
@@ -2378,12 +2397,30 @@ Section Forall2.
     (∀ x y, l !! i = Some x → k !! i = Some y → P x y → P (f x) (g y)) →
     Forall2 P (alter f i l) (alter g i k).
   Proof. intros Hl. revert i. induction Hl; intros [|]; constructor; auto. Qed.
+
   Lemma Forall2_insert l k x y i :
     Forall2 P l k → P x y → Forall2 P (<[i:=x]> l) (<[i:=y]> k).
   Proof. intros Hl. revert i. induction Hl; intros [|]; constructor; auto. Qed.
+  Lemma Forall2_inserts l k l' k' i :
+    Forall2 P l k → Forall2 P l' k' →
+    Forall2 P (list_inserts i l' l) (list_inserts i k' k).
+  Proof. intros ? H. revert i. induction H; eauto using Forall2_insert. Qed.
+
   Lemma Forall2_delete l k i :
     Forall2 P l k → Forall2 P (delete i l) (delete i k).
   Proof. intros Hl. revert i. induction Hl; intros [|]; simpl; intuition. Qed.
+  Lemma Forall2_option_list mx my :
+    option_Forall2 P mx my → Forall2 P (option_list mx) (option_list my).
+  Proof. destruct 1; by constructor. Qed.
+
+  Lemma Forall2_filter Q1 Q2 `{∀ x, Decision (Q1 x), ∀ y, Decision (Q2 y)} l k:
+    (∀ x y, P x y → Q1 x ↔ Q2 y) →
+    Forall2 P l k → Forall2 P (filter Q1 l) (filter Q2 k).
+  Proof.
+    intros HP; induction 1 as [|x y l k]; unfold filter; simpl; auto.
+    simplify_option_eq by (by rewrite <-(HP x y)); repeat constructor; auto.
+  Qed.
+
   Lemma Forall2_replicate_l k n x :
     length k = n → Forall (P x) k → Forall2 P (replicate n x) k.
   Proof. intros <-. induction 1; simpl; auto. Qed.
@@ -2393,10 +2430,14 @@ Section Forall2.
   Lemma Forall2_replicate n x y :
     P x y → Forall2 P (replicate n x) (replicate n y).
   Proof. induction n; simpl; constructor; auto. Qed.
-  Lemma Forall2_take l k n : Forall2 P l k → Forall2 P (take n l) (take n k).
-  Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
-  Lemma Forall2_drop l k n : Forall2 P l k → Forall2 P (drop n l) (drop n k).
-  Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
+
+  Lemma Forall2_reverse l k : Forall2 P l k → Forall2 P (reverse l) (reverse k).
+  Proof.
+    induction 1; rewrite ?reverse_nil, ?reverse_cons; eauto using Forall2_app.
+  Qed.
+  Lemma Forall2_last l k : Forall2 P l k → option_Forall2 P (last l) (last k).
+  Proof. induction 1 as [|????? []]; simpl; repeat constructor; auto. Qed.
+
   Lemma Forall2_resize l k x y n :
     P x y → Forall2 P l k → Forall2 P (resize n x l) (resize n y k).
   Proof.
@@ -2436,6 +2477,7 @@ Section Forall2.
     intros ?? <- ?. rewrite <-(resize_all k y) at 2.
     apply Forall2_resize_r with n; auto using Forall_true.
   Qed.
+
   Lemma Forall2_sublist_lookup_l l k n i l' :
     Forall2 P l k → sublist_lookup n i l = Some l' →
     ∃ k', sublist_lookup n i k = Some k' ∧ Forall2 P l' k'.
@@ -2475,13 +2517,7 @@ Section Forall2.
       drop_length, <-Forall2_length, Min.min_l by eauto with lia; [done|].
     rewrite drop_drop; auto using Forall2_drop.
   Qed.
-  Lemma Forall2_transitive {C} (Q : B → C → Prop) (R : A → C → Prop) l k lC :
-    (∀ x y z, P x y → Q y z → R x z) →
-    Forall2 P l k → Forall2 Q k lC → Forall2 R l lC.
-  Proof. intros ? Hl. revert lC. induction Hl; inversion_clear 1; eauto. Qed.
-  Lemma Forall2_Forall (Q : A → A → Prop) l :
-    Forall (λ x, Q x x) l → Forall2 Q l l.
-  Proof. induction 1; constructor; auto. Qed.
+
   Global Instance Forall2_dec `{dec : ∀ x y, Decision (P x y)} :
     ∀ l k, Decision (Forall2 P l k).
   Proof.
@@ -2495,8 +2531,9 @@ Section Forall2.
   Defined.
 End Forall2.
 
-Section Forall2_order.
+Section Forall2_proper.
   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).
@@ -2509,25 +2546,53 @@ Section Forall2_order.
   Proof. split; apply _. Qed.
   Global Instance: AntiSymm (=) R → AntiSymm (=) (Forall2 R).
   Proof. induction 2; inversion_clear 1; f_equal; auto. Qed.
+
   Global Instance: Proper (R ==> Forall2 R ==> Forall2 R) (::).
   Proof. by constructor. Qed.
   Global Instance: Proper (Forall2 R ==> Forall2 R ==> Forall2 R) (++).
-  Proof. repeat intro. eauto using Forall2_app. Qed.
-  Global Instance: Proper (Forall2 R ==> Forall2 R) (delete i).
-  Proof. repeat intro. eauto using Forall2_delete. Qed.
-  Global Instance: Proper (R ==> Forall2 R) (replicate n).
-  Proof. repeat intro. eauto using Forall2_replicate. Qed.
+  Proof. repeat intro. by apply Forall2_app. Qed.
+  Global Instance: Proper (Forall2 R ==> (=)) length.
+  Proof. repeat intro. eauto using Forall2_length. Qed.
+  Global Instance: Proper (Forall2 R ==> Forall2 R) tail.
+  Proof. repeat intro. eauto using Forall2_tail. Qed.
   Global Instance: Proper (Forall2 R ==> Forall2 R) (take n).
   Proof. repeat intro. eauto using Forall2_take. Qed.
   Global Instance: Proper (Forall2 R ==> Forall2 R) (drop n).
   Proof. repeat intro. eauto using Forall2_drop. Qed.
+
+  Global Instance: Proper (Forall2 R ==> option_Forall2 R) (lookup i).
+  Proof. repeat intro. by apply Forall2_lookup. Qed.
+  Global Instance:
+    Proper (R ==> R) f → Proper (Forall2 R ==> Forall2 R) (alter f i).
+  Proof. repeat intro. eauto using Forall2_alter. Qed.
+  Global Instance: Proper (R ==> Forall2 R ==> Forall2 R) (insert i).
+  Proof. repeat intro. eauto using Forall2_insert. Qed.
+  Global Instance:
+    Proper (Forall2 R ==> Forall2 R ==> Forall2 R) (list_inserts i).
+  Proof. repeat intro. eauto using Forall2_inserts. Qed.
+  Global Instance: Proper (Forall2 R ==> Forall2 R) (delete i).
+  Proof. repeat intro. eauto using Forall2_delete. Qed.
+
+  Global Instance: Proper (option_Forall2 R ==> Forall2 R) option_list.
+  Proof. repeat intro. eauto using Forall2_option_list. Qed.
+  Global Instance: ∀ P `{∀ x, Decision (P x)},
+    Proper (R ==> iff) P → Proper (Forall2 R ==> Forall2 R) (filter P).
+  Proof. repeat intro; eauto using Forall2_filter. Qed.
+
+  Global Instance: Proper (R ==> Forall2 R) (replicate n).
+  Proof. repeat intro. eauto using Forall2_replicate. Qed.
+  Global Instance: Proper (Forall2 R ==> Forall2 R) reverse.
+  Proof. repeat intro. eauto using Forall2_reverse. Qed.
+  Global Instance: Proper (Forall2 R ==> option_Forall2 R) last.
+  Proof. repeat intro. eauto using Forall2_last. Qed.
   Global Instance: Proper (R ==> Forall2 R ==> Forall2 R) (resize n).
   Proof. repeat intro. eauto using Forall2_resize. Qed.
-End Forall2_order.
+End Forall2_proper.
 
 Section Forall3.
   Context {A B C} (P : A → B → C → Prop).
   Hint Extern 0 (Forall3 _ _ _ _) => constructor.
+
   Lemma Forall3_app l1 l2 k1 k2 k1' k2' :
     Forall3 P l1 k1 k1' → Forall3 P l2 k2 k2' →
     Forall3 P (l1 ++ l2) (k1 ++ k2) (k1' ++ k2').
@@ -2610,6 +2675,74 @@ Section Forall3.
   Proof. intros Hl. revert i. induction Hl; intros [|]; auto. Qed.
 End Forall3.
 
+(** Setoids *)
+Section setoid.
+  Context `{Equiv A} `{!Equivalence ((≡) : relation A)}.
+  Implicit Types l k : list A.
+
+  Lemma equiv_Forall2 l k : l ≡ k ↔ Forall2 (≡) l k.
+  Proof. split; induction 1; constructor; auto. Qed.
+  Lemma equiv_lookup l k : l ≡ k ↔ (∀ i, l !! i ≡ k !! i).
+  Proof.
+    rewrite equiv_Forall2, Forall2_lookup.
+    by setoid_rewrite equiv_option_Forall2.
+  Qed.
+
+  Global Instance list_equivalence : Equivalence ((≡) : relation (list A)).
+  Proof.
+    split.
+    - intros l. by apply equiv_Forall2.
+    - intros l k; rewrite !equiv_Forall2; by intros.
+    - intros l1 l2 l3; rewrite !equiv_Forall2; intros; by trans l2.
+  Qed.
+  Global Instance list_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (list A).
+  Proof. induction 1; f_equal; fold_leibniz; auto. Qed.
+
+  Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A).
+  Proof. by constructor. Qed.
+  Global Instance app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@app A).
+  Proof. induction 1; intros ???; simpl; try constructor; auto. Qed.
+  Global Instance length_proper : Proper ((≡) ==> (=)) (@length A).
+  Proof. induction 1; f_equal/=; auto. Qed.
+  Global Instance tail_proper : Proper ((≡) ==> (≡)) (@tail A).
+  Proof. by destruct 1. Qed.
+  Global Instance take_proper n : Proper ((≡) ==> (≡)) (@take A n).
+  Proof. induction n; destruct 1; constructor; auto. Qed.
+  Global Instance drop_proper n : Proper ((≡) ==> (≡)) (@drop A n).
+  Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
+  Global Instance list_lookup_proper i :
+    Proper ((≡) ==> (≡)) (lookup (M:=list A) i).
+  Proof. induction i; destruct 1; simpl; f_equiv; auto. Qed.
+  Global Instance list_alter_proper f i :
+    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
+  Proof. intros. induction i; destruct 1; constructor; eauto. Qed.
+  Global Instance list_insert_proper i :
+    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list A) i).
+  Proof. intros ???; induction i; destruct 1; constructor; eauto. Qed.
+  Global Instance list_inserts_proper i :
+    Proper ((≡) ==> (≡) ==> (≡)) (@list_inserts A i).
+  Proof.
+    intros k1 k2 Hk; revert i.
+    induction Hk; intros ????; simpl; try f_equiv; naive_solver.
+  Qed.
+  Global Instance list_delete_proper i :
+    Proper ((≡) ==> (≡)) (delete (M:=list A) i).
+  Proof. induction i; destruct 1; try constructor; eauto. Qed.
+  Global Instance option_list_proper : Proper ((≡) ==> (≡)) (@option_list A).
+  Proof. destruct 1; by constructor. Qed.
+  Global Instance list_filter_proper P `{∀ x, Decision (P x)} :
+    Proper ((≡) ==> iff) P → Proper ((≡) ==> (≡)) (filter (B:=list A) P).
+  Proof. intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed.
+  Global Instance replicate_proper n : Proper ((≡) ==> (≡)) (@replicate A n).
+  Proof. induction n; constructor; auto. Qed.
+  Global Instance reverse_proper : Proper ((≡) ==> (≡)) (@reverse A).
+  Proof. induction 1; rewrite ?reverse_cons; repeat (done || f_equiv). Qed.
+  Global Instance last_proper : Proper ((≡) ==> (≡)) (@last A).
+  Proof. induction 1 as [|????? []]; simpl; repeat (done || f_equiv). Qed.
+  Global Instance resize_proper n : Proper ((≡) ==> (≡) ==> (≡)) (@resize A n).
+  Proof. induction n; destruct 2; simpl; repeat (auto || f_equiv). Qed.
+End setoid.
+
 (** * Properties of the monadic operations *)
 Section fmap.
   Context {A B : Type} (f : A → B).
@@ -2621,13 +2754,19 @@ Section fmap.
   Lemma list_fmap_ext (g : A → B) (l1 l2 : list A) :
     (∀ x, f x = g x) → l1 = l2 → fmap f l1 = fmap g l2.
   Proof. intros ? <-. induction l1; f_equal/=; auto. Qed.
+  Lemma list_fmap_setoid_ext `{Equiv B} (g : A → B) l :
+    (∀ x, f x ≡ g x) → f <$> l ≡ g <$> l.
+  Proof. induction l; constructor; auto. Qed.
+
   Global Instance: Inj (=) (=) f → Inj (=) (=) (fmap f).
   Proof.
     intros ? l1. induction l1 as [|x l1 IH]; [by intros [|??]|].
     intros [|??]; intros; f_equal/=; simplify_eq; auto.
   Qed.
+
   Definition fmap_nil : f <$> [] = [] := eq_refl.
   Definition fmap_cons x l : f <$> x :: l = f x :: f <$> l := eq_refl.
+
   Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
   Proof. by induction l1; f_equal/=. Qed.
   Lemma fmap_nil_inv k :  f <$> k = [] → k = [].
@@ -2642,6 +2781,7 @@ Section fmap.
     intros [|x l] ?; simplify_eq/=.
     destruct (IH l) as (l1&l2&->&->&->); [done|]. by exists (x :: l1), l2.
   Qed.
+
   Lemma fmap_length l : length (f <$> l) = length l.
   Proof. by induction l; f_equal/=. Qed.
   Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
@@ -2676,6 +2816,7 @@ Section fmap.
   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. intros Hl. revert i. by induction Hl; intros [|i]; f_equal/=. Qed.
+
   Lemma elem_of_list_fmap_1 l x : x ∈ l → f x ∈ f <$> l.
   Proof. induction 1; csimpl; rewrite elem_of_cons; intuition. Qed.
   Lemma elem_of_list_fmap_1_alt l x y : x ∈ l → y = f x → y ∈ f <$> l.
@@ -2690,6 +2831,7 @@ Section fmap.
   Proof.
     naive_solver eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
   Qed.
+
   Lemma NoDup_fmap_1 l : NoDup (f <$> l) → NoDup l.
   Proof.
     induction l; simpl; inversion_clear 1; constructor; auto.
@@ -2702,12 +2844,14 @@ Section fmap.
   Qed.
   Lemma NoDup_fmap `{!Inj (=) (=) f} l : NoDup (f <$> l) ↔ NoDup l.
   Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
+
   Global Instance fmap_sublist: Proper (sublist ==> sublist) (fmap f).
   Proof. induction 1; simpl; econstructor; eauto. Qed.
   Global Instance fmap_contains: Proper (contains ==> contains) (fmap f).
   Proof. induction 1; simpl; econstructor; eauto. Qed.
   Global Instance fmap_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (fmap f).
   Proof. induction 1; simpl; econstructor; eauto. Qed.
+
   Lemma Forall_fmap_ext_1 (g : A → B) (l : list A) :
     Forall (λ x, f x = g x) l → fmap f l = fmap g l.
   Proof. by induction 1; f_equal/=. Qed.
@@ -2721,6 +2865,7 @@ Section fmap.
   Proof. split; induction l; inversion_clear 1; constructor; auto. Qed.
   Lemma Exists_fmap (P : B → Prop) l : Exists P (f <$> l) ↔ Exists (P ∘ f) l.
   Proof. split; induction l; inversion 1; constructor; by auto. Qed.
+
   Lemma Forall2_fmap_l {C} (P : B → C → Prop) l1 l2 :
     Forall2 P (f <$> l1) l2 ↔ Forall2 (P ∘ f) l1 l2.
   Proof.
@@ -2740,6 +2885,7 @@ Section fmap.
   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 list_fmap_bind {C} (g : B → list C) l : (f <$> l) ≫= g = l ≫= g ∘ f.
   Proof. by induction l; f_equal/=. Qed.
 End fmap.
@@ -3468,7 +3614,7 @@ Ltac decompose_Forall := repeat
   | |- Forall _ (_ ++ _) => apply Forall_app_2
   | |- Forall _ (_ <$> _) => apply Forall_fmap
   | |- Forall _ (_ ≫= _) => apply Forall_bind
-  | |- Forall2 _ _ _ => apply Forall2_Forall
+  | |- Forall2 _ _ _ => apply Forall_Forall2
   | |- Forall2 _ [] [] => constructor
   | |- Forall2 _ (_ :: _) (_ :: _) => constructor
   | |- Forall2 _ (_ ++ _) (_ ++ _) => first
@@ -3482,7 +3628,7 @@ Ltac decompose_Forall := repeat
   | |- Forall _ _ =>
     apply Forall_lookup_2; intros ???; progress decompose_Forall_hyps
   | |- Forall2 _ _ _ =>
-    apply Forall2_lookup_2; [solve_length|];
+    apply Forall2_same_length_lookup_2; [solve_length|];
     intros ?????; progress decompose_Forall_hyps
   end.
 
diff --git a/prelude/option.v b/prelude/option.v
index 2155d932ed484de68c436347629131eba4398a4d..f6066107a320c5fbef0f27bac5d0bf76e4caedc7 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -10,69 +10,74 @@ Inductive option_reflect {A} (P : A → Prop) (Q : Prop) : option A → Type :=
 
 (** * General definitions and theorems *)
 (** Basic properties about equality. *)
-Lemma None_ne_Some {A} (a : A) : None ≠ Some a.
+Lemma None_ne_Some {A} (x : A) : None ≠ Some x.
 Proof. congruence. Qed.
-Lemma Some_ne_None {A} (a : A) : Some a ≠ None.
+Lemma Some_ne_None {A} (x : A) : Some x ≠ None.
 Proof. congruence. Qed.
-Lemma eq_None_ne_Some {A} (x : option A) a : x = None → x ≠ Some a.
+Lemma eq_None_ne_Some {A} (mx : option A) x : mx = None → mx ≠ Some x.
 Proof. congruence. Qed.
 Instance Some_inj {A} : Inj (=) (=) (@Some A).
 Proof. congruence. Qed.
 
 (** The non dependent elimination principle on the option type. *)
-Definition default {A B} (b : B) (x : option A) (f : A → B)  : B :=
-  match x with None => b | Some a => f a end.
+Definition default {A B} (y : B) (mx : option A) (f : A → B)  : B :=
+  match mx with None => y | Some x => f x end.
+Instance: Params (@default) 2.
 
 (** The [from_option] function allows us to get the value out of the option
 type by specifying a default value. *)
-Definition from_option {A} (a : A) (x : option A) : A :=
-  match x with None => a | Some b => b end.
+Definition from_option {A} (x : A) (mx : option A) : A :=
+  match mx with None => x | Some y => y end.
+Instance: Params (@from_option) 1.
 
 (** An alternative, but equivalent, definition of equality on the option
 data type. This theorem is useful to prove that two options are the same. *)
-Lemma option_eq {A} (x y : option A) : x = y ↔ ∀ a, x = Some a ↔ y = Some a.
-Proof. split; [by intros; by subst |]. destruct x, y; naive_solver. Qed.
-Lemma option_eq_1 {A} (x y : option A) a : x = y → x = Some a → y = Some a.
+Lemma option_eq {A} (mx my: option A): mx = my ↔ ∀ x, mx = Some x ↔ my = Some x.
+Proof. split; [by intros; by subst |]. destruct mx, my; naive_solver. Qed.
+Lemma option_eq_1 {A} (mx my: option A) x : mx = my → mx = Some x → my = Some x.
 Proof. congruence. Qed.
-Lemma option_eq_1_alt {A} (x y : option A) a : x = y → y = Some a → x = Some a.
+Lemma option_eq_1_alt {A} (mx my : option A) x :
+  mx = my → my = Some x → mx = Some x.
 Proof. congruence. Qed.
 
-Definition is_Some {A} (x : option A) := ∃ y, x = Some y.
-Lemma mk_is_Some {A} (x : option A) y : x = Some y → is_Some x.
+Definition is_Some {A} (mx : option A) := ∃ x, mx = Some x.
+Instance: Params (@is_Some) 1.
+
+Lemma mk_is_Some {A} (mx : option A) x : mx = Some x → is_Some mx.
 Proof. intros; red; subst; eauto. Qed.
 Hint Resolve mk_is_Some.
 Lemma is_Some_None {A} : ¬is_Some (@None A).
 Proof. by destruct 1. Qed.
 Hint Resolve is_Some_None.
 
-Instance is_Some_pi {A} (x : option A) : ProofIrrel (is_Some x).
+Instance is_Some_pi {A} (mx : option A) : ProofIrrel (is_Some mx).
 Proof.
-  set (P (y : option A) := match y with Some _ => True | _ => False end).
-  set (f x := match x return P x → is_Some x with
+  set (P (mx : option A) := match mx with Some _ => True | _ => False end).
+  set (f mx := match mx return P mx → is_Some mx with
     Some _ => λ _, ex_intro _ _ eq_refl | None => False_rect _ end).
-  set (g x (H : is_Some x) :=
-    match H return P x with ex_intro _ p => eq_rect _ _ I _ (eq_sym p) end).
-  assert (∀ x H, f x (g x H) = H) as f_g by (by intros ? [??]; subst).
-  intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct x, p1.
+  set (g mx (H : is_Some mx) :=
+    match H return P mx with ex_intro _ p => eq_rect _ _ I _ (eq_sym p) end).
+  assert (∀ mx H, f mx (g mx H) = H) as f_g by (by intros ? [??]; subst).
+  intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct mx, p1.
 Qed.
-Instance is_Some_dec {A} (x : option A) : Decision (is_Some x) :=
-  match x with
+Instance is_Some_dec {A} (mx : option A) : Decision (is_Some mx) :=
+  match mx with
   | Some x => left (ex_intro _ x eq_refl)
   | None => right is_Some_None
   end.
 
-Definition is_Some_proj {A} {x : option A} : is_Some x → A :=
-  match x with Some a => λ _, a | None => False_rect _ ∘ is_Some_None end.
-Definition Some_dec {A} (x : option A) : { a | x = Some a } + { x = None } :=
-  match x return { a | x = Some a } + { x = None } with
-  | Some a => inleft (a ↾ eq_refl _)
+Definition is_Some_proj {A} {mx : option A} : is_Some mx → A :=
+  match mx with Some x => λ _, x | None => False_rect _ ∘ is_Some_None end.
+Definition Some_dec {A} (mx : option A) : { x | mx = Some x } + { mx = None } :=
+  match mx return { x | mx = Some x } + { mx = None } with
+  | Some x => inleft (x ↾ eq_refl _)
   | None => inright eq_refl
   end.
 
-Lemma eq_None_not_Some {A} (x : option A) : x = None ↔ ¬is_Some x.
-Proof. destruct x; unfold is_Some; naive_solver. Qed.
-Lemma not_eq_None_Some `(x : option A) : x ≠ None ↔ is_Some x.
-Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed.
+Lemma eq_None_not_Some {A} (mx : option A) : mx = None ↔ ¬is_Some mx.
+Proof. destruct mx; unfold is_Some; naive_solver. Qed.
+Lemma not_eq_None_Some {A} (mx : option A) : mx ≠ None ↔ is_Some mx.
+Proof. rewrite eq_None_not_Some; apply dec_stable; tauto. Qed.
 
 (** Lifting a relation point-wise to option *)
 Inductive option_Forall2 {A B} (P: A → B → Prop) : option A → option B → Prop :=
@@ -90,7 +95,12 @@ Definition option_relation {A B} (R: A → B → Prop) (P: A → Prop) (Q: B →
 (** Setoids *)
 Section setoids.
   Context `{Equiv A} `{!Equivalence ((≡) : relation A)}.
+
   Global Instance option_equiv : Equiv (option A) := option_Forall2 (≡).
+
+  Lemma equiv_option_Forall2 mx my : mx ≡ my ↔ option_Forall2 (≡) mx my.
+  Proof. split; destruct 1; constructor; auto. Qed.
+
   Global Instance option_equivalence : Equivalence ((≡) : relation (option A)).
   Proof.
     split.
@@ -102,81 +112,86 @@ Section setoids.
   Proof. by constructor. Qed.
   Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
   Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed.
+
   Lemma equiv_None (mx : option A) : mx ≡ None ↔ mx = None.
   Proof. split; [by inversion_clear 1|by intros ->]. Qed.
-  Lemma equiv_Some (mx my : option A) x :
+  Lemma equiv_Some_inv_l (mx my : option A) x :
     mx ≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡ y.
   Proof. destruct 1; naive_solver. Qed.
+  Lemma equiv_Some_inv_r (mx my : option A) y :
+    mx ≡ my → mx = Some y → ∃ x, mx = Some x ∧ x ≡ y.
+  Proof. destruct 1; naive_solver. Qed.
+
   Global Instance is_Some_proper : Proper ((≡) ==> iff) (@is_Some A).
   Proof. inversion_clear 1; split; eauto. Qed.
+  Global Instance from_option_proper :
+    Proper ((≡) ==> (≡) ==> (≡)) (@from_option A).
+  Proof. by destruct 2. Qed.
 End setoids.
 
 (** Equality on [option] is decidable. *)
-Instance option_eq_None_dec {A} (x : option A) : Decision (x = None) :=
-  match x with Some _ => right (Some_ne_None _) | None => left eq_refl end.
-Instance option_None_eq_dec {A} (x : option A) : Decision (None = x) :=
-  match x with Some _ => right (None_ne_Some _) | None => left eq_refl end.
-Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)}
-  (x y : option A) : Decision (x = y).
+Instance option_eq_None_dec {A} (mx : option A) : Decision (mx = None) :=
+  match mx with Some _ => right (Some_ne_None _) | None => left eq_refl end.
+Instance option_None_eq_dec {A} (mx : option A) : Decision (None = mx) :=
+  match mx with Some _ => right (None_ne_Some _) | None => left eq_refl end.
+Instance option_eq_dec {A} {dec : ∀ x y : A, Decision (x = y)}
+  (mx my : option A) : Decision (mx = my).
 Proof.
  refine
-  match x, y with
-  | Some a, Some b => cast_if (decide (a = b))
+  match mx, my with
+  | Some x, Some y => cast_if (decide (x = y))
   | None, None => left _ | _, _ => right _
   end; clear dec; abstract congruence.
 Defined.
 
 (** * Monadic operations *)
 Instance option_ret: MRet option := @Some.
-Instance option_bind: MBind option := λ A B f x,
-  match x with Some a => f a | None => None end.
-Instance option_join: MJoin option := λ A x,
-  match x with Some x => x | None => None end.
+Instance option_bind: MBind option := λ A B f mx,
+  match mx with Some x => f x | None => None end.
+Instance option_join: MJoin option := λ A mmx,
+  match mmx with Some mx => mx | None => None end.
 Instance option_fmap: FMap option := @option_map.
-Instance option_guard: MGuard option := λ P dec A x,
-  match dec with left H => x H | _ => None end.
+Instance option_guard: MGuard option := λ P dec A f,
+  match dec with left H => f H | _ => None end.
 
-Lemma fmap_is_Some {A B} (f : A → B) x : is_Some (f <$> x) ↔ is_Some x.
-Proof. unfold is_Some; destruct x; naive_solver. Qed.
-Lemma fmap_Some {A B} (f : A → B) x y :
-  f <$> x = Some y ↔ ∃ x', x = Some x' ∧ y = f x'.
-Proof. destruct x; naive_solver. Qed.
-Lemma fmap_None {A B} (f : A → B) x : f <$> x = None ↔ x = None.
-Proof. by destruct x. Qed.
-Lemma option_fmap_id {A} (x : option A) : id <$> x = x.
-Proof. by destruct x. Qed.
-Lemma option_fmap_compose {A B} (f : A → B) {C} (g : B → C) x :
-  g ∘ f <$> x = g <$> f <$> x.
-Proof. by destruct x. Qed.
-Lemma option_fmap_ext {A B} (f g : A → B) x :
-  (∀ y, f y = g y) → f <$> x = g <$> x.
-Proof. destruct x; simpl; auto with f_equal. Qed.
-Lemma option_fmap_setoid_ext `{Equiv A, Equiv B} (f g : A → B) x :
-  (∀ y, f y ≡ g y) → f <$> x ≡ g <$> x.
-Proof. destruct x; constructor; auto. Qed.
-Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) x :
-  (f <$> x) ≫= g = x ≫= g ∘ f.
-Proof. by destruct x. Qed.
+Lemma fmap_is_Some {A B} (f : A → B) mx : is_Some (f <$> mx) ↔ is_Some mx.
+Proof. unfold is_Some; destruct mx; naive_solver. Qed.
+Lemma fmap_Some {A B} (f : A → B) mx y :
+  f <$> mx = Some y ↔ ∃ x, mx = Some x ∧ y = f x.
+Proof. destruct mx; naive_solver. Qed.
+Lemma fmap_None {A B} (f : A → B) mx : f <$> mx = None ↔ mx = None.
+Proof. by destruct mx. Qed.
+Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx.
+Proof. by destruct mx. Qed.
+Lemma option_fmap_compose {A B} (f : A → B) {C} (g : B → C) mx :
+  g ∘ f <$> mx = g <$> f <$> mx.
+Proof. by destruct mx. Qed.
+Lemma option_fmap_ext {A B} (f g : A → B) mx :
+  (∀ x, f x = g x) → f <$> mx = g <$> mx.
+Proof. intros; destruct mx; f_equal/=; auto. Qed.
+Lemma option_fmap_setoid_ext `{Equiv A, Equiv B} (f g : A → B) mx :
+  (∀ x, f x ≡ g x) → f <$> mx ≡ g <$> mx.
+Proof. destruct mx; constructor; auto. Qed.
+Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) mx :
+  (f <$> mx) ≫= g = mx ≫= g ∘ f.
+Proof. by destruct mx. 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_eq; csimpl; auto. Qed.
-Lemma option_bind_ext_fun {A B} (f g : A → option B) x :
-  (∀ a, f a = g a) → x ≫= f = x ≫= g.
+  (g : B → option C) (mx : option A) : (mx ≫= f) ≫= g = mx ≫= (mbind g ∘ f).
+Proof. by destruct mx; simpl. Qed.
+Lemma option_bind_ext {A B} (f g : A → option B) mx my :
+  (∀ x, f x = g x) → mx = my → mx ≫= f = my ≫= g.
+Proof. destruct mx, my; naive_solver. Qed.
+Lemma option_bind_ext_fun {A B} (f g : A → option B) mx :
+  (∀ x, f x = g x) → mx ≫= f = mx ≫= g.
 Proof. intros. by apply option_bind_ext. Qed.
-Lemma bind_Some {A B} (f : A → option B) (x : option A) b :
-  x ≫= f = Some b ↔ ∃ a, x = Some a ∧ f a = Some b.
-Proof. split. by destruct x as [a|]; [exists a|]. by intros (?&->&?). Qed.
-Lemma bind_None {A B} (f : A → option B) (x : option A) :
-  x ≫= f = None ↔ x = None ∨ ∃ a, x = Some a ∧ f a = None.
-Proof.
-  split; [|by intros [->|(?&->&?)]].
-  destruct x; intros; simplify_eq/=; eauto.
-Qed.
-Lemma bind_with_Some {A} (x : option A) : x ≫= Some = x.
-Proof. by destruct x. Qed.
+Lemma bind_Some {A B} (f : A → option B) (mx : option A) y :
+  mx ≫= f = Some y ↔ ∃ x, mx = Some x ∧ f x = Some y.
+Proof. destruct mx; naive_solver. Qed.
+Lemma bind_None {A B} (f : A → option B) (mx : option A) :
+  mx ≫= f = None ↔ mx = None ∨ ∃ x, mx = Some x ∧ f x = None.
+Proof. destruct mx; naive_solver. Qed.
+Lemma bind_with_Some {A} (mx : option A) : mx ≫= Some = mx.
+Proof. by destruct mx. Qed.
 
 (** ** Inverses of constructors *)
 (** We can do this in a fancy way using dependent types, but rewrite does
@@ -206,25 +221,26 @@ Instance maybe_Some {A} : Maybe (@Some A) := id.
 Arguments maybe_Some _ !_ /.
 
 (** * Union, intersection and difference *)
-Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
-  match x, y with
-  | Some a, Some b => f a b
-  | Some a, None => Some a
-  | None, Some b => Some b
+Instance option_union_with {A} : UnionWith A (option A) := λ f mx my,
+  match mx, my with
+  | Some x, Some y => f x y
+  | Some x, None => Some x
+  | None, Some y => Some y
   | None, None => None
   end.
 Instance option_intersection_with {A} : IntersectionWith A (option A) :=
-  λ f x y, match x, y with Some a, Some b => f a b | _, _ => None end.
-Instance option_difference_with {A} : DifferenceWith A (option A) := λ f x y,
-  match x, y with
-  | Some a, Some b => f a b
-  | Some a, None => Some a
+  λ f mx my, match mx, my with Some x, Some y => f x y | _, _ => None end.
+Instance option_difference_with {A} : DifferenceWith A (option A) := λ f mx my,
+  match mx, my with
+  | Some x, Some y => f x y
+  | Some x, None => Some x
   | None, _ => None
   end.
 Instance option_union {A} : Union (option A) := union_with (λ x _, Some x).
-Lemma option_union_Some {A} (x y : option A) z :
-  x ∪ y = Some z → x = Some z ∨ y = Some z.
-Proof. destruct x, y; intros; simplify_eq; auto. Qed.
+
+Lemma option_union_Some {A} (mx my : option A) z :
+  mx ∪ my = Some z → mx = Some z ∨ my = Some z.
+Proof. destruct mx, my; naive_solver. Qed.
 
 Section option_union_intersection_difference.
   Context {A} (f : A → A → option A).
@@ -248,61 +264,61 @@ End option_union_intersection_difference.
 Tactic Notation "case_option_guard" "as" ident(Hx) :=
   match goal with
   | H : appcontext C [@mguard option _ ?P ?dec] |- _ =>
-    change (@mguard option _ P dec) with (λ A (x : P → option A),
-      match @decide P dec with left H' => x H' | _ => None end) in *;
+    change (@mguard option _ P dec) with (λ A (f : P → option A),
+      match @decide P dec with left H' => f H' | _ => None end) in *;
     destruct_decide (@decide P dec) as Hx
   | |- appcontext C [@mguard option _ ?P ?dec] =>
-    change (@mguard option _ P dec) with (λ A (x : P → option A),
-      match @decide P dec with left H' => x H' | _ => None end) in *;
+    change (@mguard option _ P dec) with (λ A (f : P → option A),
+      match @decide P dec with left H' => f H' | _ => None end) in *;
     destruct_decide (@decide P dec) as Hx
   end.
 Tactic Notation "case_option_guard" :=
   let H := fresh in case_option_guard as H.
 
-Lemma option_guard_True {A} P `{Decision P} (x : option A) :
-  P → guard P; x = x.
+Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
+  P → guard P; mx = mx.
 Proof. intros. by case_option_guard. Qed.
-Lemma option_guard_False {A} P `{Decision P} (x : option A) :
-  ¬P → guard P; x = None.
+Lemma option_guard_False {A} P `{Decision P} (mx : option A) :
+  ¬P → guard P; mx = None.
 Proof. intros. by case_option_guard. Qed.
-Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (x : option A) :
-  (P ↔ Q) → guard P; x = guard Q; x.
+Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (mx : option A) :
+  (P ↔ Q) → guard P; mx = guard Q; mx.
 Proof. intros [??]. repeat case_option_guard; intuition. Qed.
 
 Tactic Notation "simpl_option" "by" tactic3(tac) :=
-  let assert_Some_None A o H := first
+  let assert_Some_None A mx H := first
     [ let x := fresh in evar (x:A); let x' := eval unfold x in x in clear x;
-      assert (o = Some x') as H by tac
-    | assert (o = None) as H by tac ]
+      assert (mx = Some x') as H by tac
+    | assert (mx = None) as H by tac ]
   in repeat match goal with
   | H : appcontext [@mret _ _ ?A] |- _ =>
      change (@mret _ _ A) with (@Some A) in H
   | |- appcontext [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
-  | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
-    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
-  | H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ =>
-    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
-  | H : context [default (A:=?A) _ ?o _] |- _ =>
-    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
-  | H : context [from_option (A:=?A) _ ?o] |- _ =>
-    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
-  | H : context [ match ?o with _ => _ end ] |- _ =>
-    match type of o with
+  | H : context [mbind (M:=option) (A:=?A) ?f ?mx] |- _ =>
+    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
+  | H : context [fmap (M:=option) (A:=?A) ?f ?mx] |- _ =>
+    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
+  | H : context [default (A:=?A) _ ?mx _] |- _ =>
+    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
+  | H : context [from_option (A:=?A) _ ?mx] |- _ =>
+    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
+  | H : context [ match ?mx with _ => _ end ] |- _ =>
+    match type of mx with
     | option ?A =>
-      let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
+      let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
     end
-  | |- context [mbind (M:=option) (A:=?A) ?f ?o] =>
-    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
-  | |- context [fmap (M:=option) (A:=?A) ?f ?o] =>
-    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
-  | |- context [default (A:=?A) _ ?o _] =>
-    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
-  | |- context [from_option (A:=?A) _ ?o] =>
-    let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
-  | |- context [ match ?o with _ => _ end ] =>
-    match type of o with
+  | |- context [mbind (M:=option) (A:=?A) ?f ?mx] =>
+    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
+  | |- context [fmap (M:=option) (A:=?A) ?f ?mx] =>
+    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
+  | |- context [default (A:=?A) _ ?mx _] =>
+    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
+  | |- context [from_option (A:=?A) _ ?mx] =>
+    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
+  | |- context [ match ?mx with _ => _ end ] =>
+    match type of mx with
     | option ?A =>
-      let Hx := fresh in assert_Some_None A o Hx; rewrite Hx; clear Hx
+      let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
     end
   | H : context [decide _] |- _ => rewrite decide_True in H by tac
   | H : context [decide _] |- _ => rewrite decide_False in H by tac
@@ -326,26 +342,26 @@ Tactic Notation "simplify_option_eq" "by" tactic3(tac) :=
   | _ : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
   | _ : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
   | H : _ ∪ _ = Some _ |- _ => apply option_union_Some in H; destruct H
-  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
-    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
-    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
-    let y := fresh in destruct o as [y|] eqn:?;
-      [change (f y = x) in H|change (None = x) in H]
-  | H : ?x = mbind (M:=option) ?f ?o |- _ =>
-    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
-    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
-    let y := fresh in destruct o as [y|] eqn:?;
-      [change (x = f y) in H|change (x = None) in H]
-  | H : fmap (M:=option) ?f ?o = ?x |- _ =>
-    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
-    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
-    let y := fresh in destruct o as [y|] eqn:?;
-      [change (Some (f y) = x) in H|change (None = x) in H]
-  | H : ?x = fmap (M:=option) ?f ?o |- _ =>
-    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
-    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
-    let y := fresh in destruct o as [y|] eqn:?;
-      [change (x = Some (f y)) in H|change (x = None) in H]
+  | H : mbind (M:=option) ?f ?mx = ?my |- _ =>
+    match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
+    match my with Some _ => idtac | None => idtac | _ => fail 1 end;
+    let x := fresh in destruct mx as [x|] eqn:?;
+      [change (f x = my) in H|change (None = my) in H]
+  | H : ?my = mbind (M:=option) ?f ?mx |- _ =>
+    match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
+    match my with Some _ => idtac | None => idtac | _ => fail 1 end;
+    let x := fresh in destruct mx as [x|] eqn:?;
+      [change (my = f x) in H|change (my = None) in H]
+  | H : fmap (M:=option) ?f ?mx = ?my |- _ =>
+    match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
+    match my with Some _ => idtac | None => idtac | _ => fail 1 end;
+    let x := fresh in destruct mx as [x|] eqn:?;
+      [change (Some (f x) = my) in H|change (None = my) in H]
+  | H : ?my = fmap (M:=option) ?f ?mx |- _ =>
+    match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
+    match my with Some _ => idtac | None => idtac | _ => fail 1 end;
+    let x := fresh in destruct mx as [x|] eqn:?;
+      [change (my = Some (f x)) in H|change (my = None) in H]
   | _ => progress case_decide
   | _ => progress case_option_guard
   end.