diff --git a/stdpp/fin_sets.v b/stdpp/fin_sets.v
index f21214a42e64040096ac1c50cfca69bbd0503819..41ab6c8d52591a6b6ec130091abc704bb9920a8f 100644
--- a/stdpp/fin_sets.v
+++ b/stdpp/fin_sets.v
@@ -311,7 +311,7 @@ Proof.
     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 duplicable folding over [elements (X ∩ Y)] using [foldr_idemp].
+  remove the repeated folding over [elements (X ∩ Y)] using [foldr_idemp].
   Most of the proof work concerns the side conditions of [foldr_permutation]
   and [foldr_idemp], which require relating results about lists and sets. *)
   intros ?.