From 5766024f95c231d5e5aa9672471f82b8056e9abf Mon Sep 17 00:00:00 2001
From: Niels <nnmvdw@gmail.com>
Date: Fri, 11 Aug 2017 13:15:31 +0200
Subject: [PATCH] path_ishprop now in extensionality

---
 FiniteSets/fsets/extensionality.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/FiniteSets/fsets/extensionality.v b/FiniteSets/fsets/extensionality.v
index 6f2004e..75c887d 100644
--- a/FiniteSets/fsets/extensionality.v
+++ b/FiniteSets/fsets/extensionality.v
@@ -40,7 +40,7 @@ Section ext.
     forall Y, X ⊆ X ∪ Y.
   Proof.
     hinduction X ; try (repeat (intro; intros; apply path_forall);
-                        intro ; apply equiv_hprop_allpath ; apply _).
+                        intro ; apply path_ishprop).
     - apply (fun _ => tt).
     - intros a Y.
       apply (tr(inl(tr idpath))).
@@ -69,7 +69,7 @@ Section ext.
     eapply equiv_iff_hprop_uncurried.
     split.
     - hinduction X ;
-        try (intros; repeat (apply path_forall; intro); apply equiv_hprop_allpath ; apply _).
+        try (intros; repeat (apply path_forall; intro); apply path_ishprop).
       + intros ; reflexivity.
       + intros a f.
         apply f.
@@ -89,7 +89,7 @@ Section ext.
           left.
           apply Ha.
     - hinduction X ;
-        try (intros; repeat (apply path_forall; intro); apply equiv_hprop_allpath ; apply _).
+        try (intros; repeat (apply path_forall; intro); apply path_ishprop).
       + intros. contradiction.
       + intros b f a.
         simple refine (Trunc_ind _ _) ; cbn.