From 31889d4e487060682d5ca58e5e7e19e14954fc24 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 3 Aug 2017 14:43:42 +0200
Subject: [PATCH] A short lemma [FSet A = FSetC A]

---
 FiniteSets/fsets/isomorphism.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/FiniteSets/fsets/isomorphism.v b/FiniteSets/fsets/isomorphism.v
index 253b433..e72fa58 100644
--- a/FiniteSets/fsets/isomorphism.v
+++ b/FiniteSets/fsets/isomorphism.v
@@ -66,4 +66,9 @@ Section Iso.
     unfold Sect. apply repr_iso_id_r.
   Defined.
 
-End Iso.
\ No newline at end of file
+  Theorem fset_fsetc : FSet A = FSetC A.
+  Proof.
+    apply (equiv_path _ _)^-1.
+    exact repr_iso.
+  Defined.
+End Iso.