From 2782152e485206afbf3d228f177ae4ba618530e0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 Mar 2021 20:38:34 +0100
Subject: [PATCH] Add lemma `top_infinite`.

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

diff --git a/theories/sets.v b/theories/sets.v
index 89a799b6..8e95e8d4 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1145,6 +1145,11 @@ Section more_finite.
   Proof. intros Hinf [xs ?] xs'. destruct (Hinf (xs ++ xs')). set_solver. Qed.
 End more_finite.
 
+Lemma top_infinite `{TopSet A C, Infinite A} : set_infinite (⊤ : C).
+Proof.
+  intros xs. exists (fresh xs). split; [set_solver|]. apply infinite_is_fresh.
+Qed.
+
 (** Sets of sequences of natural numbers *)
 (* The set [seq_seq start len] of natural numbers contains the sequence
 [start, start + 1, ..., start + (len-1)]. *)
-- 
GitLab