diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index abf730e1c9cc3ac65eaa9487c7a5a04e7325c23c..eb264a2c8154c5555e374e83ae3ee218158fdde5 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -3278,8 +3278,8 @@ End kmap.
 Section preimage.
   (** We restrict the theory to finite sets with Leibniz equality, which is
   sufficient for [gset], but not for [boolset] or [propset]. The result of the
-  pre-image is a map of sets. To support general sets, we need setoid equality
-  on sets, and thus setoid equality on maps. *)
+  pre-image is a map of sets. To support general sets, we would need setoid
+  equality on sets, and thus setoid equality on maps. *)
   Context `{FinMap K MK, FinMap A MA, FinSet K DK, !LeibnizEquiv DK}.
   Local Notation map_preimage :=
     (map_preimage (K:=K) (A:=A) (MKA:=MK A) (MADK:=MA DK) (DK:=DK)).