From ab48ab4a75dad0953ce89bd784b332ee638dda21 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@covariant.me>
Date: Wed, 21 Jun 2017 11:22:56 +0200
Subject: [PATCH] Decidable equality on FSets

---
 FiniteSets/Ext.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/FiniteSets/Ext.v b/FiniteSets/Ext.v
index 762cf8e..e6eb4dc 100644
--- a/FiniteSets/Ext.v
+++ b/FiniteSets/Ext.v
@@ -191,4 +191,16 @@ Proof.
         apply H2.
 Defined.
 
+(* With extensionality we can prove decidable equality *)
+Instance fsets_dec_eq `{Funext} : DecidablePaths (FSet A).
+Proof.
+  intros X Y.
+  apply (decidable_equiv ((subset Y X = true) * (subset X Y = true)) (eq_subset X Y)^-1). (* TODO: this is so slow?*)
+  destruct (Y ⊆ X), (X ⊆ Y).
+  - left. refine (idpath, idpath).
+  - right. refine (false_ne_true o snd).
+  - right. refine (false_ne_true o fst).
+  - right. refine (false_ne_true o fst).
+Defined.
+
 End ext.