From bbe8f665df6dac9f32ef50c7279a2b3ff2588764 Mon Sep 17 00:00:00 2001
From: Niels van der Weide <n.vanderweide@science.ru.nl>
Date: Thu, 21 Sep 2017 14:24:27 +0200
Subject: [PATCH] Weakened assumption of singleton_isIn_d

---
 FiniteSets/kuratowski/properties.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/FiniteSets/kuratowski/properties.v b/FiniteSets/kuratowski/properties.v
index 958fb29..3886169 100644
--- a/FiniteSets/kuratowski/properties.v
+++ b/FiniteSets/kuratowski/properties.v
@@ -320,7 +320,7 @@ Section properties_membership_decidable.
     apply comprehension_isIn_d.
   Defined.
   
-  Lemma singleton_isIn_d `{DecidablePaths A} (a b : A) :
+  Lemma singleton_isIn_d `{IsHSet A} (a b : A) :
     a ∈ {|b|} -> a = b.
   Proof.
     intros.