From 01d0908b8ac91e2ad031722a023edcd98143888d Mon Sep 17 00:00:00 2001
From: Niels van der Weide <n.vanderweide@science.ru.nl>
Date: Mon, 9 Oct 2017 13:59:59 +0200
Subject: [PATCH] Added member as exist

---
 FiniteSets/misc/dec_fset.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/FiniteSets/misc/dec_fset.v b/FiniteSets/misc/dec_fset.v
index baa0205..b295230 100644
--- a/FiniteSets/misc/dec_fset.v
+++ b/FiniteSets/misc/dec_fset.v
@@ -118,6 +118,16 @@ Section quantifiers.
   Defined.
 End quantifiers.
 
+Section exists_isIn.
+  Context {A : Type} `{Univalence}.
+
+  Theorem exist_isIn (a : A) (X : FSet A)
+    : a ∈ X = exist (fun b => BuildhProp(Trunc (-1) (a = b))) X.
+  Proof.
+    hinduction X ; try (intros ; apply path_ishprop) ; cbn ; try reflexivity.
+  Defined.
+End exists_isIn.  
+
 Section simple_example.
   Context `{Univalence}.