From fda4dbb93337da40f9eb7526ad5bb812b37eb146 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Oct 2020 20:47:02 +0100
Subject: [PATCH] add SetUnfoldElemOf instance

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

diff --git a/theories/sets.v b/theories/sets.v
index 3a81880c..8c8bfba0 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -883,6 +883,10 @@ Section fin_to_set.
 
   Lemma elem_of_fin_to_set a : a ∈ fin_to_set A.
   Proof. apply elem_of_list_to_set, elem_of_enum. Qed.
+
+  Global Instance set_unfold_fin_to_set a :
+    SetUnfoldElemOf a (fin_to_set A) True.
+  Proof. constructor. split; auto using elem_of_fin_to_set. Qed.
 End fin_to_set.
 
 
-- 
GitLab