diff --git a/theories/sets.v b/theories/sets.v
index e8bed5bb556d0c78b6e089583327dbe97081919d..33e2139589f167c34d9a2e399401ba34165ff648 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -940,6 +940,11 @@ Section pred_finite_infinite.
   Lemma pred_not_infinite_finite {A} (P : A → Prop) :
     pred_infinite P → pred_finite P → False.
   Proof. intros Hinf [xs ?]. destruct (Hinf xs). set_solver. Qed.
+
+  Lemma pred_infinite_True `{Infinite A} : pred_infinite (λ _: A, True).
+  Proof.
+    intros xs. exists (fresh xs). split; [done|]. apply infinite_is_fresh.
+  Qed.
 End pred_finite_infinite.
 
 Section set_finite_infinite.