From 74cd449f7b0c7f65a8445d75d47f4bfd97242af2 Mon Sep 17 00:00:00 2001
From: Niels <nmvdw@ip-145-116-140-192.wlan-int.ru.nl>
Date: Wed, 24 May 2017 14:52:52 +0200
Subject: [PATCH] Elements of union

---
 FiniteSets/properties.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/FiniteSets/properties.v b/FiniteSets/properties.v
index 8891de1..8b0a669 100644
--- a/FiniteSets/properties.v
+++ b/FiniteSets/properties.v
@@ -428,5 +428,11 @@ hrecursion X; try (intros ; apply set_path2).
   rewrite <- P.
   rewrite <- Q.
 Admitted.
+
+Theorem union_isIn (X Y : FSet A) (a : A) : isIn a (U X Y) = orb (isIn a X) (isIn a Y).
+Proof.
+reflexivity.  
+Defined.
+                                                                
   
 End properties.