From c04c13375c2b28d416e15e07a425675457dcce24 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 3 Mar 2019 15:47:50 +0100
Subject: [PATCH] =?UTF-8?q?Prove=20`pred=5Finfinite=20(=CE=BB=20=5F:=20A,?=
 =?UTF-8?q?=20True)`=20for=20`A`=20infinite.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/sets.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/sets.v b/theories/sets.v
index e8bed5bb..33e21395 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.
-- 
GitLab