diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index fca9f8a24f662342b700309f8f8ef24afb7c4cb2..7179c7968d5332f8a6ba192c0e3a9a5b0628c34e 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1280,6 +1280,165 @@ Proof.
     assert (m !! j = Some y) by (apply Hm; by right). naive_solver.
 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 (uncurry 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_1_1 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_1_2 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_1_1,
+      map_Forall_insert_1_2, map_Forall_insert_2.
+  Qed.
+  Lemma map_Forall_singleton (i : K) (x : A) :
+    map_Forall P ({[i := x]} : M A) â†” P i x.
+  Proof.
+    unfold map_Forall. setoid_rewrite lookup_singleton_Some. naive_solver.
+  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 (uncurry 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 [map_Exists] predicate *)
+Section map_Exists.
+  Context {A} (P : K â†’ A â†’ Prop).
+  Implicit Types m : M A.
+
+  Lemma map_Exists_to_list m : map_Exists P m â†” Exists (uncurry P) (map_to_list m).
+  Proof.
+    rewrite Exists_exists. split.
+    - intros [? [? [? ?]]]. eexists (_, _). by rewrite elem_of_map_to_list.
+    - intros [[??] [??]]. eexists _, _. by rewrite <-elem_of_map_to_list.
+  Qed.
+  Lemma map_Exists_empty : Â¬ map_Exists P (âˆ… : M A).
+  Proof. intros [?[?[Hm ?]]]. by rewrite lookup_empty in Hm. Qed.
+  Lemma map_Exists_impl (Q : K â†’ A â†’ Prop) m :
+    map_Exists P m â†’ (âˆ€ i x, P i x â†’ Q i x) â†’ map_Exists Q m.
+  Proof. unfold map_Exists; naive_solver. Qed.
+  Lemma map_Exists_insert_1 m i x :
+    map_Exists P (<[i:=x]>m) â†’ P i x âˆ¨ map_Exists P m.
+  Proof. intros [j[y[?%lookup_insert_Some ?]]]. unfold map_Exists. naive_solver. Qed.
+  Lemma map_Exists_insert_2_1 m i x : P i x â†’ map_Exists P (<[i:=x]>m).
+  Proof. intros Hm. exists i, x. by rewrite lookup_insert. Qed.
+  Lemma map_Exists_insert_2_2 m i x :
+    m !! i = None â†’ map_Exists P m â†’ map_Exists P (<[i:=x]>m).
+  Proof.
+    intros Hm [j[y[??]]]. exists j, y. by rewrite lookup_insert_ne by congruence.
+  Qed.
+  Lemma map_Exists_insert m i x :
+    m !! i = None â†’ map_Exists P (<[i:=x]>m) â†” P i x âˆ¨ map_Exists P m.
+  Proof.
+    naive_solver eauto using map_Exists_insert_1,
+      map_Exists_insert_2_1, map_Exists_insert_2_2.
+  Qed.
+  Lemma map_Exists_singleton (i : K) (x : A) :
+    map_Exists P ({[i := x]} : M A) â†” P i x.
+  Proof.
+    unfold map_Exists. setoid_rewrite lookup_singleton_Some. naive_solver.
+  Qed.
+  Lemma map_Exists_delete m i : map_Exists P (delete i m) â†’ map_Exists P m.
+  Proof.
+    intros [j [y [Hm ?]]]. rewrite lookup_delete_Some in Hm.
+    unfold map_Exists. naive_solver.
+  Qed.
+  Lemma map_Exists_lookup m :
+    map_Exists P m â†” âˆƒ i x, m !! i = Some x âˆ§ P i x.
+  Proof. done. Qed.
+  Lemma map_Exists_lookup_1 m :
+    map_Exists P m â†’ âˆƒ i x, m !! i = Some x âˆ§ P i x.
+  Proof. by rewrite map_Exists_lookup. Qed.
+  Lemma map_Exists_lookup_2 m i x :
+    m !! i = Some x â†’ P i x â†’ map_Exists P m.
+  Proof. rewrite map_Exists_lookup. by eauto. Qed.
+  Lemma map_Exists_foldr_delete m is :
+    map_Exists P (foldr delete m is) â†’ map_Exists P m.
+  Proof. induction is; eauto using map_Exists_delete. Qed.
+
+  Lemma map_Exists_ind (Q : M A â†’ Prop) :
+    (âˆ€ i x, P i x â†’ Q {[ i := x ]}) â†’
+    (âˆ€ m i x, m !! i = None â†’ map_Exists P m â†’ Q m â†’ Q (<[i:=x]>m)) â†’
+    âˆ€ m, map_Exists P m â†’ Q m.
+  Proof.
+    intros Hsingleton Hinsert m Hm. induction m as [|i x m Hi IH] using map_ind.
+    { by destruct map_Exists_empty. }
+    apply map_Exists_insert in Hm as [?|?]; [|by eauto..].
+    clear IH. induction m as [|j y m Hj IH] using map_ind; [by eauto|].
+    apply lookup_insert_None in Hi as [??].
+    rewrite insert_commute by done. apply Hinsert.
+    - by apply lookup_insert_None.
+    - apply map_Exists_insert; by eauto.
+    - eauto.
+  Qed.
+
+  Lemma map_not_Exists (m : M A) :
+    Â¬map_Exists P m â†” map_Forall (Î» i x, Â¬ P i x) m.
+  Proof. unfold map_Exists, map_Forall; naive_solver. Qed.
+
+  Context `{âˆ€ i x, Decision (P i x)}.
+  Global Instance map_Exists_dec m : Decision (map_Exists P m).
+  Proof.
+    refine (cast_if (decide (Exists (uncurry P) (map_to_list m))));
+      by rewrite map_Exists_to_list.
+  Defined.
+End map_Exists.
+
 (** ** The filter operation *)
 Section map_filter_lookup.
   Context {A} (P : K * A â†’ Prop) `{!âˆ€ x, Decision (P x)}.
@@ -1503,165 +1662,6 @@ Lemma map_filter_comm {A}
   filter P (filter Q m) = filter Q (filter P m).
 Proof. rewrite !map_filter_filter. apply map_filter_ext. naive_solver. 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 (uncurry 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_1_1 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_1_2 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_1_1,
-      map_Forall_insert_1_2, map_Forall_insert_2.
-  Qed.
-  Lemma map_Forall_singleton (i : K) (x : A) :
-    map_Forall P ({[i := x]} : M A) â†” P i x.
-  Proof.
-    unfold map_Forall. setoid_rewrite lookup_singleton_Some. naive_solver.
-  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 (uncurry 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 [map_Exists] predicate *)
-Section map_Exists.
-  Context {A} (P : K â†’ A â†’ Prop).
-  Implicit Types m : M A.
-
-  Lemma map_Exists_to_list m : map_Exists P m â†” Exists (uncurry P) (map_to_list m).
-  Proof.
-    rewrite Exists_exists. split.
-    - intros [? [? [? ?]]]. eexists (_, _). by rewrite elem_of_map_to_list.
-    - intros [[??] [??]]. eexists _, _. by rewrite <-elem_of_map_to_list.
-  Qed.
-  Lemma map_Exists_empty : Â¬ map_Exists P (âˆ… : M A).
-  Proof. intros [?[?[Hm ?]]]. by rewrite lookup_empty in Hm. Qed.
-  Lemma map_Exists_impl (Q : K â†’ A â†’ Prop) m :
-    map_Exists P m â†’ (âˆ€ i x, P i x â†’ Q i x) â†’ map_Exists Q m.
-  Proof. unfold map_Exists; naive_solver. Qed.
-  Lemma map_Exists_insert_1 m i x :
-    map_Exists P (<[i:=x]>m) â†’ P i x âˆ¨ map_Exists P m.
-  Proof. intros [j[y[?%lookup_insert_Some ?]]]. unfold map_Exists. naive_solver. Qed.
-  Lemma map_Exists_insert_2_1 m i x : P i x â†’ map_Exists P (<[i:=x]>m).
-  Proof. intros Hm. exists i, x. by rewrite lookup_insert. Qed.
-  Lemma map_Exists_insert_2_2 m i x :
-    m !! i = None â†’ map_Exists P m â†’ map_Exists P (<[i:=x]>m).
-  Proof.
-    intros Hm [j[y[??]]]. exists j, y. by rewrite lookup_insert_ne by congruence.
-  Qed.
-  Lemma map_Exists_insert m i x :
-    m !! i = None â†’ map_Exists P (<[i:=x]>m) â†” P i x âˆ¨ map_Exists P m.
-  Proof.
-    naive_solver eauto using map_Exists_insert_1,
-      map_Exists_insert_2_1, map_Exists_insert_2_2.
-  Qed.
-  Lemma map_Exists_singleton (i : K) (x : A) :
-    map_Exists P ({[i := x]} : M A) â†” P i x.
-  Proof.
-    unfold map_Exists. setoid_rewrite lookup_singleton_Some. naive_solver.
-  Qed.
-  Lemma map_Exists_delete m i : map_Exists P (delete i m) â†’ map_Exists P m.
-  Proof.
-    intros [j [y [Hm ?]]]. rewrite lookup_delete_Some in Hm.
-    unfold map_Exists. naive_solver.
-  Qed.
-  Lemma map_Exists_lookup m :
-    map_Exists P m â†” âˆƒ i x, m !! i = Some x âˆ§ P i x.
-  Proof. done. Qed.
-  Lemma map_Exists_lookup_1 m :
-    map_Exists P m â†’ âˆƒ i x, m !! i = Some x âˆ§ P i x.
-  Proof. by rewrite map_Exists_lookup. Qed.
-  Lemma map_Exists_lookup_2 m i x :
-    m !! i = Some x â†’ P i x â†’ map_Exists P m.
-  Proof. rewrite map_Exists_lookup. by eauto. Qed.
-  Lemma map_Exists_foldr_delete m is :
-    map_Exists P (foldr delete m is) â†’ map_Exists P m.
-  Proof. induction is; eauto using map_Exists_delete. Qed.
-
-  Lemma map_Exists_ind (Q : M A â†’ Prop) :
-    (âˆ€ i x, P i x â†’ Q {[ i := x ]}) â†’
-    (âˆ€ m i x, m !! i = None â†’ map_Exists P m â†’ Q m â†’ Q (<[i:=x]>m)) â†’
-    âˆ€ m, map_Exists P m â†’ Q m.
-  Proof.
-    intros Hsingleton Hinsert m Hm. induction m as [|i x m Hi IH] using map_ind.
-    { by destruct map_Exists_empty. }
-    apply map_Exists_insert in Hm as [?|?]; [|by eauto..].
-    clear IH. induction m as [|j y m Hj IH] using map_ind; [by eauto|].
-    apply lookup_insert_None in Hi as [??].
-    rewrite insert_commute by done. apply Hinsert.
-    - by apply lookup_insert_None.
-    - apply map_Exists_insert; by eauto.
-    - eauto.
-  Qed.
-
-  Lemma map_not_Exists (m : M A) :
-    Â¬map_Exists P m â†” map_Forall (Î» i x, Â¬ P i x) m.
-  Proof. unfold map_Exists, map_Forall; naive_solver. Qed.
-
-  Context `{âˆ€ i x, Decision (P i x)}.
-  Global Instance map_Exists_dec m : Decision (map_Exists P m).
-  Proof.
-    refine (cast_if (decide (Exists (uncurry P) (map_to_list m))));
-      by rewrite map_Exists_to_list.
-  Defined.
-End map_Exists.
-
 (** ** Properties of the [merge] operation *)
 Section merge.
   Context {A} (f : option A â†’ option A â†’ option A).