diff --git a/CHANGELOG.md b/CHANGELOG.md
index 688a091e46abcb87a5f88d75ed0f2738e3f9e71e..872f6b8cbdfb9447ce18f1d5dd94b0880ce55a10 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -63,6 +63,10 @@ API-breaking change is listed.
     `String.function` and `String.lemma`.
   + Add `String.le` and some theory about it (decidability, proof irrelevance,
     total order).
+- Add lemmas `foldr_idemp_strong` and `foldr_idemp`.
+- Add lemmas `set_fold_union_strong` and `set_fold_union`.
+- Add lemmas `map_fold_union_strong`, `map_fold_union`,
+  `map_fold_disj_union_strong`, `map_fold_disj_union` and `map_fold_proper`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 4f4a146307fd4e54dec03748b8d6b2cc81e7a887..504ad810af2d1105d06086c0dd4ed72f72282853 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -1567,6 +1567,19 @@ Lemma map_fold_comm_acc {A B} (f : K → A → B → B) (g : B → B) (x : B) (m
   map_fold f (g x) m = g (map_fold f x m).
 Proof. intros. apply (map_fold_comm_acc_strong _); [solve_proper|done..]. Qed.
 
+(** Not written using [Instance .. Proper] because it is ambigious to apply due
+to the arbitrary [R]. *)
+Lemma map_fold_proper {A B} (R : relation B) `{!PreOrder R}
+    (f : K → A → B → B) (b1 b2 : B) (m : M A) :
+  (∀ j z, Proper (R ==> R) (f j z)) →
+  R b1 b2 →
+  R (map_fold f b1 m) (map_fold f b2 m).
+Proof.
+  intros Hf Hb. induction m as [|i x m ?? IH] using map_first_key_ind.
+  { by rewrite !map_fold_empty. }
+  rewrite !map_fold_insert_first_key by done. by f_equiv.
+Qed.
+
 (** ** Properties of the [map_Forall] predicate *)
 Section map_Forall.
   Context {A} (P : K → A → Prop).
@@ -2987,6 +3000,92 @@ Proof.
     rewrite map_disjoint_alt in Hcd_disj; naive_solver.
 Qed.
 
+(** The following lemma shows that folding over two maps separately (using the
+result of the first fold as input for the second fold) is equivalent to folding
+over the union, *if* the function is idempotent for the elements that will be
+processed twice ([m1 ∩ m2]) and does not care about the order in which elements
+are processed.
+
+This is a generalization of [map_fold_union] (below) with a.) a relation [R]
+instead of equality b.) premises that ensure the elements are in [m1 ∪ m2]. *)
+Lemma map_fold_union_strong {A B} (R : relation B) `{!PreOrder R}
+    (f : K → A → B → B) (b : B) (m1 m2 : M A) :
+  (∀ j z, Proper (R ==> R) (f j z)) →
+  (∀ j z1 z2 y,
+    (** This is morally idempotence for elements of [m1 ∩ m2] *)
+    m1 !! j = Some z1 → m2 !! j = Some z2 →
+    (** We cannot write this in the usual direction of idempotence properties
+    (i.e., [R (f j z1 (f j z2 y)) (f j z1 y)]) because [R] is not symmetric. *)
+    R (f j z1 y) (f j z1 (f j z2 y))) →
+  (∀ j1 j2 z1 z2 y,
+    (** This is morally commutativity + associativity for elements of [m1 ∪ m2] *)
+    j1 ≠ j2 →
+    m1 !! j1 = Some z1 ∨ m2 !! j1 = Some z1 →
+    m1 !! j2 = Some z2 ∨ m2 !! j2 = Some z2 →
+    R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
+  R (map_fold f b (m1 ∪ m2)) (map_fold f (map_fold f b m2) m1).
+Proof.
+  intros Hf. revert m2.
+  induction m1 as [|j x m Hmj IH] using map_ind; intros m2 Hf_idemp Hf_assoc.
+  { by rewrite (left_id_L _ _), map_fold_empty. }
+  setoid_rewrite lookup_insert_Some in Hf_assoc.
+  setoid_rewrite lookup_insert_Some in Hf_idemp.
+  rewrite <-insert_union_l, insert_union_r,
+    <-insert_delete_insert, <-insert_union_r by done.
+  trans (f j x (map_fold f b (m ∪ delete j m2))).
+  { apply (map_fold_insert R f); [solve_proper|..].
+    - intros j1 j2 z1 z2 y ? Hj1 Hj2.
+      apply Hf_assoc; [done|revert Hj1|revert Hj2];
+        rewrite lookup_insert_Some, !lookup_union_Some_raw, lookup_delete_Some;
+        naive_solver.
+    - by rewrite lookup_union, Hmj, lookup_delete. }
+  trans (f j x (map_fold f (map_fold f b (delete j m2)) m)).
+  { apply Hf, IH.
+    - intros j' z1 z2 y ? Hj'. apply Hf_idemp; revert Hj';
+        rewrite lookup_delete_Some, ?lookup_insert_Some; naive_solver.
+    - intros j1 j2 z1 z2 y ? Hj1 Hj2.
+      apply Hf_assoc; [done|revert Hj1|revert Hj2];
+        rewrite lookup_delete_Some; clear Hf_idemp Hf_assoc; naive_solver. }
+  trans (f j x (map_fold f (map_fold f b m2) m)).
+  - destruct (m2 !! j) as [x'|] eqn:?; [|by rewrite delete_notin by done].
+    trans (f j x (f j x' (map_fold f (map_fold f b (delete j m2)) m))); [by auto|].
+    f_equiv. trans (map_fold f (f j x' (map_fold f b (delete j m2))) m).
+    + apply (map_fold_comm_acc_strong (flip R)); [solve_proper|].
+      intros; apply Hf_assoc;
+        rewrite ?lookup_union_Some_raw, ?lookup_insert_Some; naive_solver.
+    + apply map_fold_proper; [solve_proper..|].
+      apply (map_fold_delete (flip R)); [solve_proper|naive_solver..].
+  - apply (map_fold_insert (flip R)); [solve_proper| |done].
+    intros j1 j2 z1 z2 y ? Hj1 Hj2.
+    apply Hf_assoc; [done|revert Hj2|revert Hj1];
+      rewrite !lookup_insert_Some; naive_solver.
+Qed.
+Lemma map_fold_union {A B} (f : K → A → B → B) (b : B) m1 m2 :
+  (∀ j z1 z2 y, f j z1 (f j z2 y) = f j z1 y) →
+  (∀ j1 j2 z1 z2 y, f j1 z1 (f j2 z2 y) = f j2 z2 (f j1 z1 y)) →
+  map_fold f b (m1 ∪ m2) = map_fold f (map_fold f b m2) m1.
+Proof. intros. apply (map_fold_union_strong _); [solve_proper|auto..]. Qed.
+
+Lemma map_fold_disj_union_strong {A B} (R : relation B) `{!PreOrder R}
+    (f : K → A → B → B) (b : B) (m1 m2 : M A) :
+  (∀ j z, Proper (R ==> R) (f j z)) →
+  m1 ##ₘ m2 →
+  (∀ j1 j2 z1 z2 y,
+    j1 ≠ j2 →
+    m1 !! j1 = Some z1 ∨ m2 !! j1 = Some z1 →
+    m1 !! j2 = Some z2 ∨ m2 !! j2 = Some z2 →
+    R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
+  R (map_fold f b (m1 ∪ m2)) (map_fold f (map_fold f b m2) m1).
+Proof.
+  rewrite map_disjoint_spec. intros ??.
+  apply (map_fold_union_strong _); [solve_proper|naive_solver].
+Qed.
+Lemma map_fold_disj_union {A B} (f : K → A → B → B) (b : B) m1 m2 :
+  m1 ##ₘ m2 →
+  (∀ j1 j2 z1 z2 y, f j1 z1 (f j2 z2 y) = f j2 z2 (f j1 z1 y)) →
+  map_fold f b (m1 ∪ m2) = map_fold f (map_fold f b m2) m1.
+Proof. intros. apply (map_fold_disj_union_strong _); [solve_proper|auto..]. Qed.
+
 (** ** Properties of the [union_list] operation *)
 Lemma map_disjoint_union_list_l {A} (ms : list (M A)) (m : M A) :
   ⋃ ms ##ₘ m ↔ Forall (.##ₘ m) ms.
diff --git a/stdpp/fin_sets.v b/stdpp/fin_sets.v
index cc1725e3507ef05e30c071801e5b2acdf3845ff4..24ed3103e053ff52a5f0aef6e960d3a2536ffc69 100644
--- a/stdpp/fin_sets.v
+++ b/stdpp/fin_sets.v
@@ -298,28 +298,112 @@ Proof. by unfold set_fold; simpl; rewrite elements_empty. Qed.
 Lemma set_fold_singleton {B} (f : A → B → B) (b : B) (a : A) :
   set_fold f b ({[a]} : C) = f a b.
 Proof. by unfold set_fold; simpl; rewrite elements_singleton. Qed.
-(** Generalization of [set_fold_disj_union] (below) with a.) a relation [R]
+
+(** The following lemma shows that folding over two sets separately (using the
+result of the first fold as input for the second fold) is equivalent to folding
+over the union, *if* the function is idempotent for the elements that will be
+processed twice ([X ∩ Y]) and does not care about the order in which elements
+are processed.
+
+This is a generalization of [set_fold_union] (below) with a.) a relation [R]
 instead of equality b.) a function [f : A → B → B] instead of [f : A → A → A],
 and c.) premises that ensure the elements are in [X ∪ Y]. *)
-Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R}
+Lemma set_fold_union_strong {B} (R : relation B) `{!PreOrder R}
     (f : A → B → B) (b : B) X Y :
   (∀ x, Proper (R ==> R) (f x)) →
+  (∀ x b',
+    (** This is morally idempotence for elements of [X ∩ Y] *)
+    x ∈ X ∩ Y →
+    (** We cannot write this in the usual direction of idempotence properties
+    (i.e., [R (f x (f x b'))) (f x b')]) because [R] is not symmetric. *)
+    R (f x b') (f x (f x b'))) →
   (∀ x1 x2 b',
     (** This is morally commutativity + associativity for elements of [X ∪ Y] *)
     x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 →
     R (f x1 (f x2 b')) (f x2 (f x1 b'))) →
-  X ## Y →
   R (set_fold f b (X ∪ Y)) (set_fold f (set_fold f b X) Y).
 Proof.
-  intros ? Hf Hdisj. unfold set_fold; simpl.
-  rewrite <-foldr_app. apply (foldr_permutation R f b).
-  - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hf.
+  (** This lengthy proof involves various steps by transitivity of [R].
+  Roughly, we show that the LHS is related to folding over:
+
+    elements (Y ∖ X) ++ elements (X ∩ Y) ++ elements (X ∖ Y)
+
+  and the RHS is related to folding over:
+
+    elements (Y ∖ X) ++ elements (X ∩ Y) ++ elements (X ∩ Y) ++ elements (Y ∖ X)
+
+  These steps are justified by lemma [foldr_permutation]. In the middle we
+  remove the repeated folding over [elements (X ∩ Y)] using [foldr_idemp_strong].
+  Most of the proof work concerns the side conditions of [foldr_permutation]
+  and [foldr_idemp_strong], which require relating results about lists and
+  sets. *)
+  intros ?.
+  assert (∀ b1 b2 l, R b1 b2 → R (foldr f b1 l) (foldr f b2 l)) as Hff.
+  { intros b1 b2 l Hb. induction l as [|x l]; simpl; [done|]. by f_equiv. }
+  intros Hfidemp Hfcomm. unfold set_fold; simpl.
+  trans (foldr f b (elements (Y ∖ X) ++ elements (X ∩ Y) ++ elements (X ∖ Y))).
+  { apply (foldr_permutation R f b).
+    - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+      + apply elem_of_list_lookup_2 in Hj1. set_solver.
+      + apply elem_of_list_lookup_2 in Hj2. set_solver.
+      + intros ->. pose proof (NoDup_elements (X ∪ Y)).
+        by eapply Hj, NoDup_lookup.
+    - rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
+      destruct (decide (x ∈ X)), (decide (x ∈ Y)); set_solver. }
+  trans (foldr f (foldr f b (elements (X ∩ Y) ++ elements (X ∖ Y)))
+    (elements (Y ∖ X) ++ elements (X ∩ Y))).
+  { rewrite !foldr_app. apply Hff. apply (foldr_idemp_strong (flip R)).
+    - solve_proper.
+    - intros j a b' ?%elem_of_list_lookup_2. apply Hfidemp. set_solver.
+    - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+      + apply elem_of_list_lookup_2 in Hj2. set_solver.
+      + apply elem_of_list_lookup_2 in Hj1. set_solver.
+      + intros ->. pose proof (NoDup_elements (X ∩ Y)).
+        by eapply Hj, NoDup_lookup. }
+  trans (foldr f (foldr f b (elements (X ∩ Y) ++ elements (X ∖ Y))) (elements Y)).
+  { apply (foldr_permutation R f _).
+    - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+      + apply elem_of_list_lookup_2 in Hj1. set_solver.
+      + apply elem_of_list_lookup_2 in Hj2. set_solver.
+      + intros ->. assert (NoDup (elements (Y ∖ X) ++ elements (X ∩ Y))).
+        { rewrite <-elements_disj_union by set_solver. apply NoDup_elements. }
+        by eapply Hj, NoDup_lookup.
+    - rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
+      destruct (decide (x ∈ X)); set_solver. }
+  apply Hff. apply (foldr_permutation R f _).
+  - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
     + apply elem_of_list_lookup_2 in Hj1. set_solver.
     + apply elem_of_list_lookup_2 in Hj2. set_solver.
-    + intros ->. pose proof (NoDup_elements (X ∪ Y)).
+    + intros ->. assert (NoDup (elements (X ∩ Y) ++ elements (X ∖ Y))).
+      { rewrite <-elements_disj_union by set_solver. apply NoDup_elements. }
       by eapply Hj, NoDup_lookup.
-  - by rewrite elements_disj_union, (comm (++)).
+  - rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
+    destruct (decide (x ∈ Y)); set_solver.
+Qed.
+Lemma set_fold_union (f : A → A → A) (b : A) X Y :
+  IdemP (=) f →
+  Comm (=) f →
+  Assoc (=) f →
+  set_fold f b (X ∪ Y) = set_fold f (set_fold f b X) Y.
+Proof.
+  intros. apply (set_fold_union_strong _ _ _ _ _ _).
+  - intros x b' _. by rewrite (assoc_L f), (idemp f).
+  - intros x1 x2 b' _ _ _. by rewrite !(assoc_L f), (comm_L f x1).
 Qed.
+
+(** Generalization of [set_fold_disj_union] (below) with a.) a relation [R]
+instead of equality b.) a function [f : A → B → B] instead of [f : A → A → A],
+and c.) premises that ensure the elements are in [X ∪ Y]. *)
+Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R}
+    (f : A → B → B) (b : B) X Y :
+  (∀ x, Proper (R ==> R) (f x)) →
+  (∀ x1 x2 b',
+    (** This is morally commutativity + associativity for elements of [X ∪ Y] *)
+    x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 →
+    R (f x1 (f x2 b')) (f x2 (f x1 b'))) →
+  X ## Y →
+  R (set_fold f b (X ∪ Y)) (set_fold f (set_fold f b X) Y).
+Proof. intros. apply set_fold_union_strong; set_solver. Qed.
 Lemma set_fold_disj_union (f : A → A → A) (b : A) X Y :
   Comm (=) f →
   Assoc (=) f →
diff --git a/stdpp/list.v b/stdpp/list.v
index a9b537ab392c0045c2d3b46551e8e131367679c6..cc68e9067b51e7837644201cca60cf351f3940e1 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -4659,6 +4659,7 @@ Proof.
     symmetry in Hl12; apply Permutation_inj in Hl12 as [_ (g&?&Hg)].
     apply (Hf' (g j1) _ (g j2)); [naive_solver|by rewrite <-Hg..].
 Qed.
+
 Lemma foldr_permutation_proper {A B} (R : relation B) `{!PreOrder R}
     (f : A → B → B) (b : B) `{!∀ x, Proper (R ==> R) (f x)}
     (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
@@ -4694,6 +4695,46 @@ Proof.
   intros j1 a1 j2 a2 b _ _ _. by rewrite !(assoc_L f), (comm_L f a1).
 Qed.
 
+(** The following lemma shows that folding over a list twice (using the result
+of the first fold as input for the second fold) is equivalent to folding over
+the list once, *if* the function is idempotent for the elements of the list
+and does not care about the order in which elements are processed. *)
+Lemma foldr_idemp_strong {A B} (R : relation B) `{!PreOrder R}
+    (f : A → B → B) (b : B) `{!∀ x, Proper (R ==> R) (f x)} (l : list A) :
+  (∀ j a b,
+    (** This is morally idempotence for elements of [l] *)
+    l !! j = Some a →
+    R (f a (f a b)) (f a b)) →
+  (∀ j1 a1 j2 a2 b,
+    (** This is morally commutativity + associativity for elements of [l] *)
+    j1 ≠ j2 → l !! j1 = Some a1 → l !! j2 = Some a2 →
+    R (f a1 (f a2 b)) (f a2 (f a1 b))) →
+  R (foldr f (foldr f b l) l) (foldr f b l).
+Proof.
+  intros Hfidem Hfcomm. induction l as [|x l IH]; simpl; [done|].
+  trans (f x (f x (foldr f (foldr f b l) l))).
+  { f_equiv. rewrite <-foldr_snoc, <-foldr_cons.
+    apply (foldr_permutation (flip R) f).
+    - solve_proper.
+    - intros j1 a1 j2 a2 b' ???. by apply (Hfcomm j2 _ j1).
+    - by rewrite <-Permutation_cons_append. }
+  rewrite <-foldr_cons.
+  trans (f x (f x (foldr f b l))); [|by apply (Hfidem 0)].
+  simpl. do 2 f_equiv. apply IH.
+  - intros j a b' ?. by apply (Hfidem (S j)).
+  - intros j1 a1 j2 a2 b' ???. apply (Hfcomm (S j1) _ (S j2)); auto with lia.
+Qed.
+Lemma foldr_idemp {A} (f : A → A → A) (a : A) (l : list A) :
+  IdemP (=) f →
+  Assoc (=) f →
+  Comm (=) f →
+  foldr f (foldr f a l) l = foldr f a l.
+Proof.
+  intros. apply (foldr_idemp_strong (=) f a).
+  - intros j a1 a2 _. by rewrite (assoc_L f), (idemp f).
+  - intros x1 a1 x2 a2 a3 _ _ _. by rewrite !(assoc_L f), (comm_L f a1).
+Qed.
+
 Lemma foldr_comm_acc_strong {A B} (R : relation B) `{!PreOrder R}
     (f : A → B → B) (g : B → B) b l :
   (∀ x, Proper (R ==> R) (f x)) →