From 4f656cac497e496e9b7531cbc5e5356e26202e2e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 23 Sep 2022 16:07:27 +0000
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

---
 stdpp/fin_sets.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stdpp/fin_sets.v b/stdpp/fin_sets.v
index f21214a4..41ab6c8d 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 ?.
-- 
GitLab