diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index fc2ff66069b1cd17c3dbd438771f7f8d29fc6014..ee0f2f3c36f92a0028ba91ad88f2757c0cde4562 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -110,27 +110,49 @@ instance, such as lists. *)
 Global Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 20 :=
   λ m1 m2, ∀ i, m1 !! i ≡ m2 !! i.
 
+(** [map_Forall], [map_Exists] are defined in terms of [map_fold] so that they
+can be used in nested recursive fixpoints, see [tests/fin_maps.v] for examples.
+This is typically not the definition that is useful in proofs. The lemmas
+[map_Forall_lookup] or [map_Exists_lookup] provide nicer equivalent definitions.
+So in proofs it is prefered to [rewrite] with [map_Forall_lookup] or
+[map_Exists_lookup] instead of [unfold]ing these definitions directly. *)
 Definition map_Forall `{MapFold K A M} (P : K → A → Prop) : M → Prop :=
   map_fold (λ i x, and (P i x)) True.
-
 Definition map_Exists `{MapFold K A M} (P : K → A → Prop) : M → Prop :=
   map_fold (λ i x, or (P i x)) False.
 
-Definition map_relation `{∀ A, Lookup K A (M A)} {A B} (R : A → B → Prop)
-    (P : A → Prop) (Q : B → Prop) (m1 : M A) (m2 : M B) : Prop := ∀ i,
-  option_relation R P Q (m1 !! i) (m2 !! i).
-Definition map_included `{∀ A, Lookup K A (M A)} {A}
-  (R : relation A) : relation (M A) := map_relation R (λ _, False) (λ _, True).
-Definition map_agree `{∀ A, Lookup K A (M A)} {A} : relation (M A) :=
-  map_relation (=) (λ _, True) (λ _, True).
-Definition map_disjoint `{∀ A, Lookup K A (M A)} {A} : relation (M A) :=
-  map_relation (λ _ _, False) (λ _, True) (λ _, True).
+(** Similarly, [map_relation] and [map_included] are defined in terms of
+[map_Forall] so they can be used in nested recursive fixpoints. See also
+[tests/fin_maps.v] for examples *)
+Local Definition map_relation_pred {A B}
+    (R : A → B → Prop) (P : A → Prop) (Q : B → Prop)
+    (mx : option A) (my : option B) : option Prop :=
+  match mx, my with
+  | Some x, Some y => Some (R x y)
+  | Some x, None => Some (P x)
+  | None, Some y => Some (Q y)
+  | None, None => None
+  end.
+Definition map_relation `{Merge M, ∀ A, MapFold K A (M A)} {A B} (R : A → B → Prop)
+    (P : A → Prop) (Q : B → Prop) (m1 : M A) (m2 : M B) : Prop :=
+  map_Forall (λ _ P, P) (merge (map_relation_pred R P Q) m1 m2).
+Definition map_included `{Merge M, ∀ A, MapFold K A (M A)} {A}
+    (R : relation A) : relation (M A) :=
+  map_relation R (λ _, False) (λ _, True).
+
+(* [map_subseteq], [map_agree], and [map_disjoint] are not higher-order (do not
+have predicates as arguments), so they cannot be used in nested recursive
+fixpoints. We therefore use the nice/convenient definition. *)
+Global Instance map_subseteq `{Lookup K A M} : SubsetEq M :=
+  λ m1 m2, ∀ i x, m1 !! i = Some x → m2 !! i = Some x.
+Definition map_agree `{Lookup K A M} : relation M :=
+  λ m1 m2, ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → x = y.
+Definition map_disjoint `{Lookup K A M} : relation M :=
+  λ m1 m2, ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → False.
 Infix "##ₘ" := map_disjoint (at level 70) : stdpp_scope.
 Global Hint Extern 0 (_ ##ₘ _) => symmetry; eassumption : core.
 Notation "( m ##ₘ.)" := (map_disjoint m) (only parsing) : stdpp_scope.
 Notation "(.##ₘ m )" := (λ m2, m2 ##ₘ m) (only parsing) : stdpp_scope.
-Global Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
-  map_included (=).
 
 (** The union of two finite maps only has a meaningful definition for maps
 that are disjoint. However, as working with partial functions is inconvenient
@@ -221,26 +243,18 @@ Context `{FinMap K M}.
 (** ** General properties *)
 Lemma map_eq_iff {A} (m1 m2 : M A) : m1 = m2 ↔ ∀ i, m1 !! i = m2 !! i.
 Proof. split; [by intros ->|]. apply map_eq. Qed.
+
 Lemma map_subseteq_spec {A} (m1 m2 : M A) :
   m1 ⊆ m2 ↔ ∀ i x, m1 !! i = Some x → m2 !! i = Some x.
-Proof.
-  unfold subseteq, map_subseteq, map_relation. split; intros Hm i;
-    specialize (Hm i); destruct (m1 !! i), (m2 !! i); naive_solver.
-Qed.
-Global Instance map_included_preorder {A} (R : relation A) :
-  PreOrder R → PreOrder (map_included R : relation (M A)).
-Proof.
-  split; [intros m i; by destruct (m !! i); simpl|].
-  intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i).
-  destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_eq/=;
-    done || etrans; eauto.
-Qed.
+Proof. done. Qed.
 Global Instance map_subseteq_po {A} : PartialOrder (⊆@{M A}).
 Proof.
-  split; [apply _|].
-  intros m1 m2; rewrite !map_subseteq_spec.
-  intros; apply map_eq; intros i; apply option_eq; naive_solver.
+  split.
+  - split; repeat intro; naive_solver.
+  - intros m1 m2. rewrite !map_subseteq_spec, map_eq_iff.
+    intros; apply option_eq; naive_solver.
 Qed.
+
 Lemma lookup_total_alt `{!Inhabited A} (m : M A) i :
   m !!! i = default inhabitant (m !! i).
 Proof. reflexivity. Qed.
@@ -570,13 +584,6 @@ Proof.
   intros; apply map_eq; intros j; destruct (decide (i = j)) as [->|];
     by rewrite ?lookup_insert, ?lookup_insert_ne by done.
 Qed.
-Lemma insert_included {A} R `{!Reflexive R} (m : M A) i x :
-  (∀ y, m !! i = Some y → R y x) → map_included R m (<[i:=x]>m).
-Proof.
-  intros ? j; destruct (decide (i = j)) as [->|].
-  - rewrite lookup_insert. destruct (m !! j); simpl; eauto.
-  - rewrite lookup_insert_ne by done. by destruct (m !! j); simpl.
-Qed.
 Lemma insert_empty {A} i (x : A) : <[i:=x]> ∅ =@{M A} {[i := x]}.
 Proof. done. Qed.
 Lemma insert_non_empty {A} (m : M A) i x : <[i:=x]>m ≠ ∅.
@@ -2174,21 +2181,38 @@ Proof.
 Qed.
 
 (** ** Properties on the [map_relation] relation *)
-Section Forall2.
+Lemma map_relation_lookup {A B} (R : A → B → Prop) (P : A → Prop) (Q : B → Prop)
+    (m1 : M A) (m2 : M B) :
+  map_relation R P Q m1 m2 ↔
+    ∀ i, match m1 !! i, m2 !! i with
+         | Some x, Some y => R x y
+         | Some x, None => P x
+         | None, Some y => Q y
+         | None, None => True
+         end.
+Proof.
+  unfold map_relation. rewrite map_Forall_lookup.
+  apply forall_proper; intros i. rewrite lookup_merge.
+  destruct (m1 !! i), (m2 !! i); naive_solver.
+Qed.
+
+Section Forall2_dec.
   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 :=
+  Local Definition map_relation_bool_pred (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).
+    map_relation R P Q m1 m2 ↔
+      map_Forall (λ _, Is_true) (merge map_relation_bool_pred m1 m2).
   Proof.
-    rewrite map_Forall_lookup. split.
+    rewrite map_relation_lookup, map_Forall_lookup. split.
     - intros Hm i P'; rewrite lookup_merge; intros.
       specialize (Hm i). destruct (m1 !! i), (m2 !! i);
         simplify_eq/=; auto using bool_decide_pack.
@@ -2198,12 +2222,13 @@ Section Forall2.
   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))));
+    refine (λ m1 m2, cast_if
+      (decide (map_Forall (λ _, Is_true) (merge map_relation_bool_pred 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) :
+  Lemma map_not_relation (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)
@@ -2213,18 +2238,48 @@ Section Forall2.
     - rewrite map_relation_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i.
       rewrite lookup_merge in Hm.
       destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack.
-    - unfold map_relation, option_relation.
+    - rewrite map_relation_lookup.
       by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm;
         specialize (Hm i); simplify_option_eq.
   Qed.
-End Forall2.
+End Forall2_dec.
 
-(** ** Properties of the [map_agree] operation *)
-Lemma map_agree_spec {A} (m1 m2 : M A) :
-  map_agree m1 m2 ↔ ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → x = y.
+(** ** Properties on the [map_included] relation *)
+Lemma map_included_lookup {A} (R : relation A) (m1 m2 : M A) :
+  map_included R m1 m2 ↔
+    ∀ i, match m1 !! i, m2 !! i with
+         | Some x, Some y => R x y
+         | Some x, None => False
+         | None, _ => True
+         end.
 Proof.
-  apply forall_proper; intros i; destruct (m1 !! i), (m2 !! i); naive_solver.
+  unfold map_included. rewrite map_relation_lookup.
+  apply forall_proper; intros i. by destruct (m1 !! i), (m2 !! i).
 Qed.
+
+Global Instance map_included_preorder {A} (R : relation A) :
+  PreOrder R → PreOrder (map_included R : relation (M A)).
+Proof.
+  split.
+  - intros m. rewrite map_included_lookup. intros i. by destruct (m !! i).
+  - intros m1 m2 m3. rewrite !map_included_lookup.
+    intros Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i).
+    destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_eq/=;
+      done || etrans; eauto.
+Qed.
+
+Lemma insert_included {A} R `{!Reflexive R} (m : M A) i x :
+  (∀ y, m !! i = Some y → R y x) → map_included R m (<[i:=x]>m).
+Proof.
+  rewrite map_included_lookup. intros ? j; destruct (decide (i = j)) as [->|].
+  - rewrite lookup_insert. destruct (m !! j); simpl; eauto.
+  - rewrite lookup_insert_ne by done. by destruct (m !! j); simpl.
+Qed.
+
+(** ** Properties of the [map_agree] relation *)
+Lemma map_agree_spec {A} (m1 m2 : M A) :
+  map_agree m1 m2 ↔ ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → x = y.
+Proof. done. Qed.
 Lemma map_agree_alt {A} (m1 m2 : M A) :
   map_agree m1 m2 ↔ ∀ i, m1 !! i = None ∨ m2 !! i = None ∨ m1 !! i = m2 !! i.
 Proof.
@@ -2233,8 +2288,12 @@ Qed.
 Lemma map_not_agree {A} (m1 m2 : M A) `{!EqDecision A}:
   ¬map_agree m1 m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2 ∧ x1 ≠ x2.
 Proof.
-  unfold map_agree. rewrite map_not_Forall2 by solve_decision. naive_solver.
+  trans (¬ map_relation (=) (λ _, True) (λ _, True) m1 m2).
+  - f_equiv. rewrite map_relation_lookup. apply forall_proper; intros i.
+    destruct (m1 !! i), (m2 !! i); naive_solver.
+  - rewrite map_not_relation by solve_decision. naive_solver.
 Qed.
+
 Global Instance map_agree_refl {A} : Reflexive (map_agree : relation (M A)).
 Proof. intros ?. rewrite !map_agree_spec. naive_solver. Qed.
 Global Instance map_agree_sym {A} : Symmetric (map_agree : relation (M A)).
@@ -2311,9 +2370,7 @@ Proof. rewrite !map_agree_spec. setoid_rewrite lookup_omap_Some. naive_solver. Q
 (** ** Properties on the disjoint maps *)
 Lemma map_disjoint_spec {A} (m1 m2 : M A) :
   m1 ##ₘ m2 ↔ ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → False.
-Proof.
-  apply forall_proper; intros i; destruct (m1 !! i), (m2 !! i); naive_solver.
-Qed.
+Proof. done. Qed.
 Lemma map_disjoint_alt {A} (m1 m2 : M A) :
   m1 ##ₘ m2 ↔ ∀ i, m1 !! i = None ∨ m2 !! i = None.
 Proof.
@@ -2322,9 +2379,12 @@ Qed.
 Lemma map_not_disjoint {A} (m1 m2 : M A) :
   ¬m1 ##ₘ m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2.
 Proof.
-  unfold disjoint, map_disjoint. rewrite map_not_Forall2 by solve_decision.
-  naive_solver.
+  trans (¬ map_relation (λ _ _, False) (λ _, True) (λ _, True) m1 m2).
+  - f_equiv. rewrite map_relation_lookup. apply forall_proper; intros i.
+    destruct (m1 !! i), (m2 !! i); naive_solver.
+  - rewrite map_not_relation by solve_decision. naive_solver.
 Qed.
+
 Global Instance map_disjoint_sym {A} : Symmetric (map_disjoint : relation (M A)).
 Proof. intros m1 m2. rewrite !map_disjoint_spec. naive_solver. Qed.
 Lemma map_disjoint_empty_l {A} (m : M A) : ∅ ##ₘ m.
@@ -3092,7 +3152,7 @@ Lemma map_disjoint_difference_l {A} (m1 m2 m3 : M A) : m3 ⊆ m2 → m1 ∖ m2 #
 Proof.
   intros Hm i; specialize (Hm i).
   unfold difference, map_difference; rewrite lookup_difference_with.
-  by destruct (m1 !! i), (m2 !! i), (m3 !! i).
+  destruct (m1 !! i), (m2 !! i), (m3 !! i); naive_solver.
 Qed.
 Lemma map_disjoint_difference_r {A} (m1 m2 m3 : M A) : m3 ⊆ m2 → m3 ##ₘ m1 ∖ m2.
 Proof. intros. symmetry. by apply map_disjoint_difference_l. Qed.
@@ -3286,7 +3346,7 @@ Section setoid.
     Proper ((≡@{M A}) ==> (≡@{M A}) ==> iff) map_disjoint.
   Proof.
     intros m1 m1' Hm1 m2 m2' Hm2; split;
-      intros Hm i; specialize (Hm i); by destruct (Hm1 i), (Hm2 i).
+      intros Hm i; specialize (Hm i); destruct (Hm1 i), (Hm2 i); naive_solver.
   Qed.
   Global Instance map_fmap_proper `{Equiv B} :
     Proper (((≡) ==> (≡)) ==> (≡@{M A}) ==> (≡@{M B})) fmap.
diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index 0f47cbc779f78b3b8bdfb1dccc22c7cedfc2358e..9d7559fb46018331b558cc7cdc12a57062201ce7 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -657,6 +657,7 @@ Section more_lemmas.
     X ⊆ Y ↔
     map_relation Pos.le (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y).
   Proof.
+    rewrite map_relation_lookup.
     apply forall_proper; intros x. unfold multiplicity.
     destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia.
   Qed.