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

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

diff --git a/theories/sets.v b/theories/sets.v
index f0d23ef7..89a799b6 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1108,6 +1108,8 @@ Section set_finite_infinite.
   Proof. intros [l ?]; exists l; set_solver. Qed.
   Lemma union_finite_inv_r X Y : set_finite (X ∪ Y) → set_finite Y.
   Proof. intros [l ?]; exists l; set_solver. Qed.
+  Lemma list_to_set_finite l : set_finite (list_to_set (C:=C) l).
+  Proof. exists l. intros x. by rewrite elem_of_list_to_set. Qed.
 
   Global Instance set_infinite_subseteq :
     Proper ((⊆) ==> impl) (@set_infinite A C _).
-- 
GitLab