diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 5c7477b54d8684f6a02adf3b75a839d7b5847141..504ad810af2d1105d06086c0dd4ed72f72282853 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -3000,13 +3000,25 @@ 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 →
diff --git a/stdpp/fin_sets.v b/stdpp/fin_sets.v
index 5feab4f3061620c466d4cdfb3f9fec6c33a673b7..24ed3103e053ff52a5f0aef6e960d3a2536ffc69 100644
--- a/stdpp/fin_sets.v
+++ b/stdpp/fin_sets.v
@@ -299,7 +299,13 @@ 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_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_union_strong {B} (R : relation B) `{!PreOrder R}
diff --git a/stdpp/list.v b/stdpp/list.v
index cb42adc2c59174d64537f34e46839f0f1a652dfe..cc68e9067b51e7837644201cca60cf351f3940e1 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -4695,6 +4695,10 @@ 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,