diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 0453473c771a488bb4cd173409e894367083108c..10bd2a24593681b2005706f8ad3656c6b81585f7 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1296,177 +1296,177 @@ Qed.
 
 (** ** Properties of the [map_Forall] predicate *)
 Section map_Forall.
-Context {A} (P : K → A → Prop).
-Implicit Types m : M A.
-
-Lemma map_Forall_to_list m : map_Forall P m ↔ Forall (curry P) (map_to_list m).
-Proof.
-  rewrite Forall_forall. split.
-  - intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x).
-  - intros Hforall i x. rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)).
-Qed.
-Lemma map_Forall_empty : map_Forall P (∅ : M A).
-Proof. intros i x. by rewrite lookup_empty. Qed.
-Lemma map_Forall_impl (Q : K → A → Prop) m :
-  map_Forall P m → (∀ i x, P i x → Q i x) → map_Forall Q m.
-Proof. unfold map_Forall; naive_solver. Qed.
-Lemma map_Forall_insert_11 m i x : map_Forall P (<[i:=x]>m) → P i x.
-Proof. intros Hm. by apply Hm; rewrite lookup_insert. Qed.
-Lemma map_Forall_insert_12 m i x :
-  m !! i = None → map_Forall P (<[i:=x]>m) → map_Forall P m.
-Proof.
-  intros ? Hm j y ?; apply Hm. by rewrite lookup_insert_ne by congruence.
-Qed.
-Lemma map_Forall_insert_2 m i x :
-  P i x → map_Forall P m → map_Forall P (<[i:=x]>m).
-Proof. intros ?? j y; rewrite lookup_insert_Some; naive_solver. Qed.
-Lemma map_Forall_insert m i x :
-  m !! i = None → map_Forall P (<[i:=x]>m) ↔ P i x ∧ map_Forall P m.
-Proof.
-  naive_solver eauto using map_Forall_insert_11,
-    map_Forall_insert_12, map_Forall_insert_2.
-Qed.
-Lemma map_Forall_delete m i : map_Forall P m → map_Forall P (delete i m).
-Proof. intros Hm j x; rewrite lookup_delete_Some. naive_solver. Qed.
-Lemma map_Forall_lookup m :
-  map_Forall P m ↔ ∀ i x, m !! i = Some x → P i x.
-Proof. done. Qed.
-Lemma map_Forall_lookup_1 m i x :
-  map_Forall P m → m !! i = Some x → P i x.
-Proof. intros ?. by apply map_Forall_lookup. Qed.
-Lemma map_Forall_lookup_2 m :
-  (∀ i x, m !! i = Some x → P i x) → map_Forall P m.
-Proof. intros ?. by apply map_Forall_lookup. Qed.
-Lemma map_Forall_foldr_delete m is :
-  map_Forall P m → map_Forall P (foldr delete m is).
-Proof. induction is; eauto using map_Forall_delete. Qed.
-Lemma map_Forall_ind (Q : M A → Prop) :
-  Q ∅ →
-  (∀ m i x, m !! i = None → P i x → map_Forall P m → Q m → Q (<[i:=x]>m)) →
-  ∀ m, map_Forall P m → Q m.
-Proof.
-  intros Hnil Hinsert m. induction m using map_ind; auto.
-  rewrite map_Forall_insert by done; intros [??]; eauto.
-Qed.
-
-Context `{∀ i x, Decision (P i x)}.
-Global Instance map_Forall_dec m : Decision (map_Forall P m).
-Proof.
-  refine (cast_if (decide (Forall (curry P) (map_to_list m))));
-    by rewrite map_Forall_to_list.
-Defined.
-Lemma map_not_Forall (m : M A) :
-  ¬map_Forall P m ↔ ∃ i x, m !! i = Some x ∧ ¬P i x.
-Proof.
-  split; [|intros (i&x&?&?) Hm; specialize (Hm i x); tauto].
-  rewrite map_Forall_to_list. intros Hm.
-  apply (not_Forall_Exists _), Exists_exists in Hm.
-  destruct Hm as ([i x]&?&?). exists i, x. by rewrite <-elem_of_map_to_list.
-Qed.
+  Context {A} (P : K → A → Prop).
+  Implicit Types m : M A.
+
+  Lemma map_Forall_to_list m : map_Forall P m ↔ Forall (curry P) (map_to_list m).
+  Proof.
+    rewrite Forall_forall. split.
+    - intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x).
+    - intros Hforall i x. rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)).
+  Qed.
+  Lemma map_Forall_empty : map_Forall P (∅ : M A).
+  Proof. intros i x. by rewrite lookup_empty. Qed.
+  Lemma map_Forall_impl (Q : K → A → Prop) m :
+    map_Forall P m → (∀ i x, P i x → Q i x) → map_Forall Q m.
+  Proof. unfold map_Forall; naive_solver. Qed.
+  Lemma map_Forall_insert_11 m i x : map_Forall P (<[i:=x]>m) → P i x.
+  Proof. intros Hm. by apply Hm; rewrite lookup_insert. Qed.
+  Lemma map_Forall_insert_12 m i x :
+    m !! i = None → map_Forall P (<[i:=x]>m) → map_Forall P m.
+  Proof.
+    intros ? Hm j y ?; apply Hm. by rewrite lookup_insert_ne by congruence.
+  Qed.
+  Lemma map_Forall_insert_2 m i x :
+    P i x → map_Forall P m → map_Forall P (<[i:=x]>m).
+  Proof. intros ?? j y; rewrite lookup_insert_Some; naive_solver. Qed.
+  Lemma map_Forall_insert m i x :
+    m !! i = None → map_Forall P (<[i:=x]>m) ↔ P i x ∧ map_Forall P m.
+  Proof.
+    naive_solver eauto using map_Forall_insert_11,
+      map_Forall_insert_12, map_Forall_insert_2.
+  Qed.
+  Lemma map_Forall_delete m i : map_Forall P m → map_Forall P (delete i m).
+  Proof. intros Hm j x; rewrite lookup_delete_Some. naive_solver. Qed.
+  Lemma map_Forall_lookup m :
+    map_Forall P m ↔ ∀ i x, m !! i = Some x → P i x.
+  Proof. done. Qed.
+  Lemma map_Forall_lookup_1 m i x :
+    map_Forall P m → m !! i = Some x → P i x.
+  Proof. intros ?. by apply map_Forall_lookup. Qed.
+  Lemma map_Forall_lookup_2 m :
+    (∀ i x, m !! i = Some x → P i x) → map_Forall P m.
+  Proof. intros ?. by apply map_Forall_lookup. Qed.
+  Lemma map_Forall_foldr_delete m is :
+    map_Forall P m → map_Forall P (foldr delete m is).
+  Proof. induction is; eauto using map_Forall_delete. Qed.
+  Lemma map_Forall_ind (Q : M A → Prop) :
+    Q ∅ →
+    (∀ m i x, m !! i = None → P i x → map_Forall P m → Q m → Q (<[i:=x]>m)) →
+    ∀ m, map_Forall P m → Q m.
+  Proof.
+    intros Hnil Hinsert m. induction m using map_ind; auto.
+    rewrite map_Forall_insert by done; intros [??]; eauto.
+  Qed.
+
+  Context `{∀ i x, Decision (P i x)}.
+  Global Instance map_Forall_dec m : Decision (map_Forall P m).
+  Proof.
+    refine (cast_if (decide (Forall (curry P) (map_to_list m))));
+      by rewrite map_Forall_to_list.
+  Defined.
+  Lemma map_not_Forall (m : M A) :
+    ¬map_Forall P m ↔ ∃ i x, m !! i = Some x ∧ ¬P i x.
+  Proof.
+    split; [|intros (i&x&?&?) Hm; specialize (Hm i x); tauto].
+    rewrite map_Forall_to_list. intros Hm.
+    apply (not_Forall_Exists _), Exists_exists in Hm.
+    destruct Hm as ([i x]&?&?). exists i, x. by rewrite <-elem_of_map_to_list.
+  Qed.
 End map_Forall.
 
 (** ** Properties of the [merge] operation *)
 Section merge.
-Context {A} (f : option A → option A → option A) `{!DiagNone f}.
-Implicit Types m : M A.
-
-Global Instance: LeftId (=) None f → LeftId (=) (∅ : M A) (merge f).
-Proof.
-  intros ??. apply map_eq. intros.
-  by rewrite !(lookup_merge f), lookup_empty, (left_id_L None f).
-Qed.
-Global Instance: RightId (=) None f → RightId (=) (∅ : M A) (merge f).
-Proof.
-  intros ??. apply map_eq. intros.
-  by rewrite !(lookup_merge f), lookup_empty, (right_id_L None f).
-Qed.
-Global Instance: LeftAbsorb (=) None f → LeftAbsorb (=) (∅ : M A) (merge f).
-Proof.
-  intros ??. apply map_eq. intros.
-  by rewrite !(lookup_merge f), lookup_empty, (left_absorb_L None f).
-Qed.
-Global Instance: RightAbsorb (=) None f → RightAbsorb (=) (∅ : M A) (merge f).
-Proof.
-  intros ??. apply map_eq. intros.
-  by rewrite !(lookup_merge f), lookup_empty, (right_absorb_L None f).
-Qed.
-Lemma merge_comm m1 m2 :
-  (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) →
-  merge f m1 m2 = merge f m2 m1.
-Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
-Global Instance merge_comm' : Comm (=) f → Comm (=@{M _}) (merge f).
-Proof. intros ???. apply merge_comm. intros. by apply (comm f). Qed.
-Lemma merge_assoc m1 m2 m3 :
-  (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) =
-        f (f (m1 !! i) (m2 !! i)) (m3 !! i)) →
-  merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
-Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
-Global Instance merge_assoc' : Assoc (=) f → Assoc (=@{M _}) (merge f).
-Proof. intros ????. apply merge_assoc. intros. by apply (assoc_L f). Qed.
-Lemma merge_idemp m1 :
-  (∀ i, f (m1 !! i) (m1 !! i) = m1 !! i) → merge f m1 m1 = m1.
-Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
-Global Instance merge_idemp' : IdemP (=) f → IdemP (=@{M _}) (merge f).
-Proof. intros ??. apply merge_idemp. intros. by apply (idemp f). Qed.
+  Context {A} (f : option A → option A → option A) `{!DiagNone f}.
+  Implicit Types m : M A.
+
+  Global Instance: LeftId (=) None f → LeftId (=) (∅ : M A) (merge f).
+  Proof.
+    intros ??. apply map_eq. intros.
+    by rewrite !(lookup_merge f), lookup_empty, (left_id_L None f).
+  Qed.
+  Global Instance: RightId (=) None f → RightId (=) (∅ : M A) (merge f).
+  Proof.
+    intros ??. apply map_eq. intros.
+    by rewrite !(lookup_merge f), lookup_empty, (right_id_L None f).
+  Qed.
+  Global Instance: LeftAbsorb (=) None f → LeftAbsorb (=) (∅ : M A) (merge f).
+  Proof.
+    intros ??. apply map_eq. intros.
+    by rewrite !(lookup_merge f), lookup_empty, (left_absorb_L None f).
+  Qed.
+  Global Instance: RightAbsorb (=) None f → RightAbsorb (=) (∅ : M A) (merge f).
+  Proof.
+    intros ??. apply map_eq. intros.
+    by rewrite !(lookup_merge f), lookup_empty, (right_absorb_L None f).
+  Qed.
+  Lemma merge_comm m1 m2 :
+    (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) →
+    merge f m1 m2 = merge f m2 m1.
+  Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
+  Global Instance merge_comm' : Comm (=) f → Comm (=@{M _}) (merge f).
+  Proof. intros ???. apply merge_comm. intros. by apply (comm f). Qed.
+  Lemma merge_assoc m1 m2 m3 :
+    (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) =
+          f (f (m1 !! i) (m2 !! i)) (m3 !! i)) →
+    merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
+  Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
+  Global Instance merge_assoc' : Assoc (=) f → Assoc (=@{M _}) (merge f).
+  Proof. intros ????. apply merge_assoc. intros. by apply (assoc_L f). Qed.
+  Lemma merge_idemp m1 :
+    (∀ i, f (m1 !! i) (m1 !! i) = m1 !! i) → merge f m1 m1 = m1.
+  Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
+  Global Instance merge_idemp' : IdemP (=) f → IdemP (=@{M _}) (merge f).
+  Proof. intros ??. apply merge_idemp. intros. by apply (idemp f). Qed.
 End merge.
 
 Section more_merge.
-Context {A B C} (f : option A → option B → option C) `{!DiagNone f}.
-
-Lemma merge_Some (m1 : M A) (m2 : M B) (m : M C) :
-  (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m.
-Proof.
-  split; [|intros <-; apply (lookup_merge _) ].
-  intros Hlookup. apply map_eq; intros. rewrite Hlookup. apply (lookup_merge _).
-Qed.
-Lemma merge_empty : merge f (∅ : M A) (∅ : M B) = ∅.
-Proof. apply map_eq. intros. by rewrite !(lookup_merge f), !lookup_empty. Qed.
-Lemma partial_alter_merge g g1 g2 (m1 : M A) (m2 : M B) i :
-  g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (g2 (m2 !! i)) →
-  partial_alter g i (merge f m1 m2) =
-    merge f (partial_alter g1 i m1) (partial_alter g2 i m2).
-Proof.
-  intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
-  - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
-  - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
-Qed.
-Lemma partial_alter_merge_l g g1 (m1 : M A) (m2 : M B) i :
-  g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (m2 !! i) →
-  partial_alter g i (merge f m1 m2) = merge f (partial_alter g1 i m1) m2.
-Proof.
-  intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
-  - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
-  - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
-Qed.
-Lemma partial_alter_merge_r g g2 (m1 : M A) (m2 : M B) i :
-  g (f (m1 !! i) (m2 !! i)) = f (m1 !! i) (g2 (m2 !! i)) →
-  partial_alter g i (merge f m1 m2) = merge f m1 (partial_alter g2 i m2).
-Proof.
-  intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
-  - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
-  - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
-Qed.
-Lemma insert_merge (m1 : M A) (m2 : M B) i x y z :
-  f (Some y) (Some z) = Some x →
-  <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]>m1) (<[i:=z]>m2).
-Proof. by intros; apply partial_alter_merge. Qed.
-Lemma delete_merge (m1 : M A) (m2 : M B) i :
-  delete i (merge f m1 m2) = merge f (delete i m1) (delete i m2).
-Proof. by intros; apply partial_alter_merge. Qed.
-Lemma merge_singleton i x y z :
-  f (Some y) (Some z) = Some x →
-  merge f ({[i := y]} : M A) ({[i := z]} : M B) = {[i := x]}.
-Proof.
-  intros. by erewrite <-!insert_empty, <-insert_merge, merge_empty by eauto.
-Qed.
-Lemma insert_merge_l (m1 : M A) (m2 : M B) i x y :
-  f (Some y) (m2 !! i) = Some x →
-  <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]>m1) m2.
-Proof. by intros; apply partial_alter_merge_l. Qed.
-Lemma insert_merge_r (m1 : M A) (m2 : M B) i x z :
-  f (m1 !! i) (Some z) = Some x →
-  <[i:=x]>(merge f m1 m2) = merge f m1 (<[i:=z]>m2).
-Proof. by intros; apply partial_alter_merge_r. Qed.
+  Context {A B C} (f : option A → option B → option C) `{!DiagNone f}.
+
+  Lemma merge_Some (m1 : M A) (m2 : M B) (m : M C) :
+    (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m.
+  Proof.
+    split; [|intros <-; apply (lookup_merge _) ].
+    intros Hlookup. apply map_eq; intros. rewrite Hlookup. apply (lookup_merge _).
+  Qed.
+  Lemma merge_empty : merge f (∅ : M A) (∅ : M B) = ∅.
+  Proof. apply map_eq. intros. by rewrite !(lookup_merge f), !lookup_empty. Qed.
+  Lemma partial_alter_merge g g1 g2 (m1 : M A) (m2 : M B) i :
+    g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (g2 (m2 !! i)) →
+    partial_alter g i (merge f m1 m2) =
+      merge f (partial_alter g1 i m1) (partial_alter g2 i m2).
+  Proof.
+    intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
+    - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
+    - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
+  Qed.
+  Lemma partial_alter_merge_l g g1 (m1 : M A) (m2 : M B) i :
+    g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (m2 !! i) →
+    partial_alter g i (merge f m1 m2) = merge f (partial_alter g1 i m1) m2.
+  Proof.
+    intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
+    - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
+    - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
+  Qed.
+  Lemma partial_alter_merge_r g g2 (m1 : M A) (m2 : M B) i :
+    g (f (m1 !! i) (m2 !! i)) = f (m1 !! i) (g2 (m2 !! i)) →
+    partial_alter g i (merge f m1 m2) = merge f m1 (partial_alter g2 i m2).
+  Proof.
+    intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
+    - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
+    - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
+  Qed.
+  Lemma insert_merge (m1 : M A) (m2 : M B) i x y z :
+    f (Some y) (Some z) = Some x →
+    <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]>m1) (<[i:=z]>m2).
+  Proof. by intros; apply partial_alter_merge. Qed.
+  Lemma delete_merge (m1 : M A) (m2 : M B) i :
+    delete i (merge f m1 m2) = merge f (delete i m1) (delete i m2).
+  Proof. by intros; apply partial_alter_merge. Qed.
+  Lemma merge_singleton i x y z :
+    f (Some y) (Some z) = Some x →
+    merge f ({[i := y]} : M A) ({[i := z]} : M B) = {[i := x]}.
+  Proof.
+    intros. by erewrite <-!insert_empty, <-insert_merge, merge_empty by eauto.
+  Qed.
+  Lemma insert_merge_l (m1 : M A) (m2 : M B) i x y :
+    f (Some y) (m2 !! i) = Some x →
+    <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]>m1) m2.
+  Proof. by intros; apply partial_alter_merge_l. Qed.
+  Lemma insert_merge_r (m1 : M A) (m2 : M B) i x z :
+    f (m1 !! i) (Some z) = Some x →
+    <[i:=x]>(merge f m1 m2) = merge f m1 (<[i:=z]>m2).
+  Proof. by intros; apply partial_alter_merge_r. Qed.
 End more_merge.
 
 (** Properties of the zip_with function *)
@@ -1548,48 +1548,48 @@ Qed.
 
 (** ** Properties on the [map_relation] relation *)
 Section Forall2.
-Context {A B} (R : A → B → Prop) (P : A → Prop) (Q : B → Prop).
-Context `{∀ x y, Decision (R x y), ∀ x, Decision (P x), ∀ y, Decision (Q y)}.
-
-Let f (mx : option A) (my : option B) : option bool :=
-  match mx, my with
-  | Some x, Some y => Some (bool_decide (R x y))
-  | Some x, None => Some (bool_decide (P x))
-  | None, Some y => Some (bool_decide (Q y))
-  | None, None => None
-  end.
-Lemma map_relation_alt (m1 : M A) (m2 : M B) :
-  map_relation R P Q m1 m2 ↔ map_Forall (λ _, Is_true) (merge f m1 m2).
-Proof.
-  split.
-  - intros Hm i P'; rewrite lookup_merge by done; intros.
-    specialize (Hm i). destruct (m1 !! i), (m2 !! i);
-      simplify_eq/=; auto using bool_decide_pack.
-  - intros Hm i. specialize (Hm i). rewrite lookup_merge in Hm by done.
-    destruct (m1 !! i), (m2 !! i); simplify_eq/=; auto;
-      by eapply bool_decide_unpack, Hm.
-Qed.
-Global Instance map_relation_dec : RelDecision (map_relation (M:=M) R P Q).
-Proof.
-  refine (λ m1 m2, cast_if (decide (map_Forall (λ _, Is_true) (merge f m1 m2))));
-    abstract by rewrite map_relation_alt.
-Defined.
-(** Due to the finiteness of finite maps, we can extract a witness if the
-relation does not hold. *)
-Lemma map_not_Forall2 (m1 : M A) (m2 : M B) :
-  ¬map_relation R P Q m1 m2 ↔ ∃ i,
-    (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ ¬R x y)
-    ∨ (∃ x, m1 !! i = Some x ∧ m2 !! i = None ∧ ¬P x)
-    ∨ (∃ y, m1 !! i = None ∧ m2 !! i = Some y ∧ ¬Q y).
-Proof.
-  split.
-  - rewrite map_relation_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i.
-    rewrite lookup_merge in Hm by done.
-    destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack.
-  - unfold map_relation, option_relation.
-    by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm;
-      specialize (Hm i); simplify_option_eq.
-Qed.
+  Context {A B} (R : A → B → Prop) (P : A → Prop) (Q : B → Prop).
+  Context `{∀ x y, Decision (R x y), ∀ x, Decision (P x), ∀ y, Decision (Q y)}.
+
+  Let f (mx : option A) (my : option B) : option bool :=
+    match mx, my with
+    | Some x, Some y => Some (bool_decide (R x y))
+    | Some x, None => Some (bool_decide (P x))
+    | None, Some y => Some (bool_decide (Q y))
+    | None, None => None
+    end.
+  Lemma map_relation_alt (m1 : M A) (m2 : M B) :
+    map_relation R P Q m1 m2 ↔ map_Forall (λ _, Is_true) (merge f m1 m2).
+  Proof.
+    split.
+    - intros Hm i P'; rewrite lookup_merge by done; intros.
+      specialize (Hm i). destruct (m1 !! i), (m2 !! i);
+        simplify_eq/=; auto using bool_decide_pack.
+    - intros Hm i. specialize (Hm i). rewrite lookup_merge in Hm by done.
+      destruct (m1 !! i), (m2 !! i); simplify_eq/=; auto;
+        by eapply bool_decide_unpack, Hm.
+  Qed.
+  Global Instance map_relation_dec : RelDecision (map_relation (M:=M) R P Q).
+  Proof.
+    refine (λ m1 m2, cast_if (decide (map_Forall (λ _, Is_true) (merge f m1 m2))));
+      abstract by rewrite map_relation_alt.
+  Defined.
+  (** Due to the finiteness of finite maps, we can extract a witness if the
+  relation does not hold. *)
+  Lemma map_not_Forall2 (m1 : M A) (m2 : M B) :
+    ¬map_relation R P Q m1 m2 ↔ ∃ i,
+      (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ ¬R x y)
+      ∨ (∃ x, m1 !! i = Some x ∧ m2 !! i = None ∧ ¬P x)
+      ∨ (∃ y, m1 !! i = None ∧ m2 !! i = Some y ∧ ¬Q y).
+  Proof.
+    split.
+    - rewrite map_relation_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i.
+      rewrite lookup_merge in Hm by done.
+      destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack.
+    - unfold map_relation, option_relation.
+      by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm;
+        specialize (Hm i); simplify_option_eq.
+  Qed.
 End Forall2.
 
 (** ** Properties on the disjoint maps *)
@@ -1667,87 +1667,87 @@ Qed.
 
 (** ** Properties of the [union_with] operation *)
 Section union_with.
-Context {A} (f : A → A → option A).
-Implicit Types m : M A.
-
-Lemma lookup_union_with m1 m2 i :
-  union_with f m1 m2 !! i = union_with f (m1 !! i) (m2 !! i).
-Proof. by rewrite <-(lookup_merge _). Qed.
-Lemma lookup_union_with_Some m1 m2 i z :
-  union_with f m1 m2 !! i = Some z ↔
-    (m1 !! i = Some z ∧ m2 !! i = None) ∨
-    (m1 !! i = None ∧ m2 !! i = Some z) ∨
-    (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
-Proof.
-  rewrite lookup_union_with.
-  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
-Qed.
-Global Instance: LeftId (=@{M A}) ∅ (union_with f).
-Proof. unfold union_with, map_union_with. apply _. Qed.
-Global Instance: RightId (=@{M A}) ∅ (union_with f).
-Proof. unfold union_with, map_union_with. apply _. Qed.
-Lemma union_with_comm m1 m2 :
-  (∀ i x y, m1 !! i = Some x → m2 !! i = Some y → f x y = f y x) →
-  union_with f m1 m2 = union_with f m2 m1.
-Proof.
-  intros. apply (merge_comm _). intros i.
-  destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
-Qed.
-Global Instance: Comm (=) f → Comm (=@{M A}) (union_with f).
-Proof. intros ???. apply union_with_comm. eauto. Qed.
-Lemma union_with_idemp m :
-  (∀ i x, m !! i = Some x → f x x = Some x) → union_with f m m = m.
-Proof.
-  intros. apply (merge_idemp _). intros i.
-  destruct (m !! i) eqn:?; simpl; eauto.
-Qed.
-Lemma alter_union_with (g : A → A) m1 m2 i :
-  (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f (g x) (g y)) →
-  alter g i (union_with f m1 m2) =
-    union_with f (alter g i m1) (alter g i m2).
-Proof.
-  intros. apply (partial_alter_merge _).
-  destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
-Qed.
-Lemma alter_union_with_l (g : A → A) m1 m2 i :
-  (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f (g x) y) →
-  (∀ y, m1 !! i = None → m2 !! i = Some y → g y = y) →
-  alter g i (union_with f m1 m2) = union_with f (alter g i m1) m2.
-Proof.
-  intros. apply (partial_alter_merge_l _).
-  destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; f_equal/=; auto.
-Qed.
-Lemma alter_union_with_r (g : A → A) m1 m2 i :
-  (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f x (g y)) →
-  (∀ x, m1 !! i = Some x → m2 !! i = None → g x = x) →
-  alter g i (union_with f m1 m2) = union_with f m1 (alter g i m2).
-Proof.
-  intros. apply (partial_alter_merge_r _).
-  destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; f_equal/=; auto.
-Qed.
-Lemma delete_union_with m1 m2 i :
-  delete i (union_with f m1 m2) = union_with f (delete i m1) (delete i m2).
-Proof. by apply (partial_alter_merge _). Qed.
-Lemma foldr_delete_union_with (m1 m2 : M A) is :
-  foldr delete (union_with f m1 m2) is =
-    union_with f (foldr delete m1 is) (foldr delete m2 is).
-Proof. induction is as [|?? IHis]; simpl; [done|]. by rewrite IHis, delete_union_with. Qed.
-Lemma insert_union_with m1 m2 i x y z :
-  f x y = Some z →
-  <[i:=z]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) (<[i:=y]>m2).
-Proof. by intros; apply (partial_alter_merge _). Qed.
-Lemma insert_union_with_l m1 m2 i x :
-  m2 !! i = None → <[i:=x]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) m2.
-Proof.
-  intros Hm2. unfold union_with, map_union_with.
-  by erewrite (insert_merge_l _) by (by rewrite Hm2).
-Qed.
-Lemma insert_union_with_r m1 m2 i x :
-  m1 !! i = None → <[i:=x]>(union_with f m1 m2) = union_with f m1 (<[i:=x]>m2).
-Proof.
-  intros Hm1. unfold union_with, map_union_with.
-  by erewrite (insert_merge_r _) by (by rewrite Hm1).
-Qed.
+  Context {A} (f : A → A → option A).
+  Implicit Types m : M A.
+
+  Lemma lookup_union_with m1 m2 i :
+    union_with f m1 m2 !! i = union_with f (m1 !! i) (m2 !! i).
+  Proof. by rewrite <-(lookup_merge _). Qed.
+  Lemma lookup_union_with_Some m1 m2 i z :
+    union_with f m1 m2 !! i = Some z ↔
+      (m1 !! i = Some z ∧ m2 !! i = None) ∨
+      (m1 !! i = None ∧ m2 !! i = Some z) ∨
+      (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
+  Proof.
+    rewrite lookup_union_with.
+    destruct (m1 !! i), (m2 !! i); compute; naive_solver.
+  Qed.
+  Global Instance: LeftId (=@{M A}) ∅ (union_with f).
+  Proof. unfold union_with, map_union_with. apply _. Qed.
+  Global Instance: RightId (=@{M A}) ∅ (union_with f).
+  Proof. unfold union_with, map_union_with. apply _. Qed.
+  Lemma union_with_comm m1 m2 :
+    (∀ i x y, m1 !! i = Some x → m2 !! i = Some y → f x y = f y x) →
+    union_with f m1 m2 = union_with f m2 m1.
+  Proof.
+    intros. apply (merge_comm _). intros i.
+    destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
+  Qed.
+  Global Instance: Comm (=) f → Comm (=@{M A}) (union_with f).
+  Proof. intros ???. apply union_with_comm. eauto. Qed.
+  Lemma union_with_idemp m :
+    (∀ i x, m !! i = Some x → f x x = Some x) → union_with f m m = m.
+  Proof.
+    intros. apply (merge_idemp _). intros i.
+    destruct (m !! i) eqn:?; simpl; eauto.
+  Qed.
+  Lemma alter_union_with (g : A → A) m1 m2 i :
+    (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f (g x) (g y)) →
+    alter g i (union_with f m1 m2) =
+      union_with f (alter g i m1) (alter g i m2).
+  Proof.
+    intros. apply (partial_alter_merge _).
+    destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
+  Qed.
+  Lemma alter_union_with_l (g : A → A) m1 m2 i :
+    (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f (g x) y) →
+    (∀ y, m1 !! i = None → m2 !! i = Some y → g y = y) →
+    alter g i (union_with f m1 m2) = union_with f (alter g i m1) m2.
+  Proof.
+    intros. apply (partial_alter_merge_l _).
+    destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; f_equal/=; auto.
+  Qed.
+  Lemma alter_union_with_r (g : A → A) m1 m2 i :
+    (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f x (g y)) →
+    (∀ x, m1 !! i = Some x → m2 !! i = None → g x = x) →
+    alter g i (union_with f m1 m2) = union_with f m1 (alter g i m2).
+  Proof.
+    intros. apply (partial_alter_merge_r _).
+    destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; f_equal/=; auto.
+  Qed.
+  Lemma delete_union_with m1 m2 i :
+    delete i (union_with f m1 m2) = union_with f (delete i m1) (delete i m2).
+  Proof. by apply (partial_alter_merge _). Qed.
+  Lemma foldr_delete_union_with (m1 m2 : M A) is :
+    foldr delete (union_with f m1 m2) is =
+      union_with f (foldr delete m1 is) (foldr delete m2 is).
+  Proof. induction is as [|?? IHis]; simpl; [done|]. by rewrite IHis, delete_union_with. Qed.
+  Lemma insert_union_with m1 m2 i x y z :
+    f x y = Some z →
+    <[i:=z]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) (<[i:=y]>m2).
+  Proof. by intros; apply (partial_alter_merge _). Qed.
+  Lemma insert_union_with_l m1 m2 i x :
+    m2 !! i = None → <[i:=x]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) m2.
+  Proof.
+    intros Hm2. unfold union_with, map_union_with.
+    by erewrite (insert_merge_l _) by (by rewrite Hm2).
+  Qed.
+  Lemma insert_union_with_r m1 m2 i x :
+    m1 !! i = None → <[i:=x]>(union_with f m1 m2) = union_with f m1 (<[i:=x]>m2).
+  Proof.
+    intros Hm1. unfold union_with, map_union_with.
+    by erewrite (insert_merge_r _) by (by rewrite Hm1).
+  Qed.
 End union_with.
 
 (** ** Properties of the [union] operation *)
@@ -2056,56 +2056,56 @@ Proof. intro. by rewrite map_disjoint_list_to_map_zip_r. Qed.
 
 (** ** Properties of the [intersection_with] operation *)
 Section intersection_with.
-Context {A} (f : A → A → option A).
-Implicit Type (m: M A).
-Global Instance : LeftAbsorb (=@{M A}) ∅ (intersection_with f).
-Proof. unfold intersection_with, map_intersection_with. apply _. Qed.
-Global Instance: RightAbsorb (=@{M A}) ∅ (intersection_with f).
-Proof. unfold intersection_with, map_intersection_with. apply _. Qed.
-Lemma lookup_intersection_with m1 m2 i :
-  intersection_with f m1 m2 !! i = intersection_with f (m1 !! i) (m2 !! i).
-Proof. by rewrite <-(lookup_merge _). Qed.
-Lemma lookup_intersection_with_Some m1 m2 i z :
-  intersection_with f m1 m2 !! i = Some z ↔
-    (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
-Proof.
-  rewrite lookup_intersection_with.
-  destruct (m1 !! i), (m2 !! i); compute; naive_solver.
-Qed.
-Lemma intersection_with_comm m1 m2 :
-  (∀ i x y, m1 !! i = Some x → m2 !! i = Some y → f x y = f y x) →
-  intersection_with f m1 m2 = intersection_with f m2 m1.
-Proof.
-  intros. apply (merge_comm _). intros i.
-  destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
-Qed.
-Global Instance: Comm (=) f → Comm (=@{M A}) (intersection_with f).
-Proof. intros ???. apply intersection_with_comm. eauto. Qed.
-Lemma intersection_with_idemp m :
-  (∀ i x, m !! i = Some x → f x x = Some x) → intersection_with f m m = m.
-Proof.
-  intros. apply (merge_idemp _). intros i.
-  destruct (m !! i) eqn:?; simpl; eauto.
-Qed.
-Lemma alter_intersection_with (g : A → A) m1 m2 i :
-  (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f (g x) (g y)) →
-  alter g i (intersection_with f m1 m2) =
-    intersection_with f (alter g i m1) (alter g i m2).
-Proof.
-  intros. apply (partial_alter_merge _).
-  destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
-Qed.
-Lemma delete_intersection_with m1 m2 i :
-  delete i (intersection_with f m1 m2) = intersection_with f (delete i m1) (delete i m2).
-Proof. by apply (partial_alter_merge _). Qed.
-Lemma foldr_delete_intersection_with (m1 m2 : M A) is :
-  foldr delete (intersection_with f m1 m2) is =
-    intersection_with f (foldr delete m1 is) (foldr delete m2 is).
-Proof. induction is as [|?? IHis]; simpl; [done|]. by rewrite IHis, delete_intersection_with. Qed.
-Lemma insert_intersection_with m1 m2 i x y z :
-  f x y = Some z →
-  <[i:=z]>(intersection_with f m1 m2) = intersection_with f (<[i:=x]>m1) (<[i:=y]>m2).
-Proof. by intros; apply (partial_alter_merge _). Qed.
+  Context {A} (f : A → A → option A).
+  Implicit Type (m: M A).
+  Global Instance : LeftAbsorb (=@{M A}) ∅ (intersection_with f).
+  Proof. unfold intersection_with, map_intersection_with. apply _. Qed.
+  Global Instance: RightAbsorb (=@{M A}) ∅ (intersection_with f).
+  Proof. unfold intersection_with, map_intersection_with. apply _. Qed.
+  Lemma lookup_intersection_with m1 m2 i :
+    intersection_with f m1 m2 !! i = intersection_with f (m1 !! i) (m2 !! i).
+  Proof. by rewrite <-(lookup_merge _). Qed.
+  Lemma lookup_intersection_with_Some m1 m2 i z :
+    intersection_with f m1 m2 !! i = Some z ↔
+      (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
+  Proof.
+    rewrite lookup_intersection_with.
+    destruct (m1 !! i), (m2 !! i); compute; naive_solver.
+  Qed.
+  Lemma intersection_with_comm m1 m2 :
+    (∀ i x y, m1 !! i = Some x → m2 !! i = Some y → f x y = f y x) →
+    intersection_with f m1 m2 = intersection_with f m2 m1.
+  Proof.
+    intros. apply (merge_comm _). intros i.
+    destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
+  Qed.
+  Global Instance: Comm (=) f → Comm (=@{M A}) (intersection_with f).
+  Proof. intros ???. apply intersection_with_comm. eauto. Qed.
+  Lemma intersection_with_idemp m :
+    (∀ i x, m !! i = Some x → f x x = Some x) → intersection_with f m m = m.
+  Proof.
+    intros. apply (merge_idemp _). intros i.
+    destruct (m !! i) eqn:?; simpl; eauto.
+  Qed.
+  Lemma alter_intersection_with (g : A → A) m1 m2 i :
+    (∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f (g x) (g y)) →
+    alter g i (intersection_with f m1 m2) =
+      intersection_with f (alter g i m1) (alter g i m2).
+  Proof.
+    intros. apply (partial_alter_merge _).
+    destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
+  Qed.
+  Lemma delete_intersection_with m1 m2 i :
+    delete i (intersection_with f m1 m2) = intersection_with f (delete i m1) (delete i m2).
+  Proof. by apply (partial_alter_merge _). Qed.
+  Lemma foldr_delete_intersection_with (m1 m2 : M A) is :
+    foldr delete (intersection_with f m1 m2) is =
+      intersection_with f (foldr delete m1 is) (foldr delete m2 is).
+  Proof. induction is as [|?? IHis]; simpl; [done|]. by rewrite IHis, delete_intersection_with. Qed.
+  Lemma insert_intersection_with m1 m2 i x y z :
+    f x y = Some z →
+    <[i:=z]>(intersection_with f m1 m2) = intersection_with f (<[i:=x]>m1) (<[i:=y]>m2).
+  Proof. by intros; apply (partial_alter_merge _). Qed.
 End intersection_with.
 
 (** ** Properties of the [intersection] operation *)