diff --git a/theories/sets.v b/theories/sets.v
index 28f75fe70908fbc970cbbbb460f571c20ff6ac35..7dd881a052e4a83f5df272b150478b93e7c06011 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1046,7 +1046,7 @@ Section pred_finite_infinite.
 
   (** If [f] is surjective onto [P], then pre-composing with [f] preserves
   infinity. *)
-  Lemma pred_infinite_surj {A} (P : A → Prop) (f : A → A) :
+  Lemma pred_infinite_surj {A B} (P : B → Prop) (f : A → B) :
     (∀ x, P x → ∃ y, f y = x) →
     pred_infinite P → pred_infinite (P ∘ f).
   Proof.