From 2a561d49834b312e1359bb407375b87fdd34f3f1 Mon Sep 17 00:00:00 2001
From: Niels <nmvdw@MacBook-Air-van-Niels.local>
Date: Thu, 25 May 2017 22:21:19 +0200
Subject: [PATCH] Finished proof of extensionality

---
 FiniteSets/properties.v | 24 ++++++++++++++++--------
 1 file changed, 16 insertions(+), 8 deletions(-)

diff --git a/FiniteSets/properties.v b/FiniteSets/properties.v
index d89510c..8e8e38b 100644
--- a/FiniteSets/properties.v
+++ b/FiniteSets/properties.v
@@ -618,15 +618,23 @@ Proof.
     exact _.
     exact _.
     split ; apply subset_isIn.
-  - eapply equiv_functor_prod'.
-    apply HPropEquiv.
+  - apply HPropEquiv.
     exact _.
     exact _.
-    split ; apply subset_isIn.
-    apply HPropEquiv.
-    exact _.
-    exact _.
-    split ; apply subset_isIn.'. 
-Admitted.
+    split.
+    * intros [H1 H2 a].
+      specialize (H1 a) ; specialize (H2 a).
+      destruct (isIn a X).
+      + symmetry ; apply (H2 idpath).
+      + destruct (isIn a Y).
+        { apply (H1 idpath). }
+        { reflexivity. }
+    * intros H1.
+      split ; intro a ; intro H2.
+      + rewrite (H1 a).
+        apply H2.
+      + rewrite <- (H1 a).
+        apply H2.
+Defined.
 
 End properties.