From 5728445c3e60866223596b2e25a3b24b137e79b1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 29 Jan 2021 17:23:28 +0100
Subject: [PATCH] generalize to two different types

---
 theories/sets.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/sets.v b/theories/sets.v
index 28f75fe7..7dd881a0 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.
-- 
GitLab