diff --git a/FiniteSets/kuratowski/length.v b/FiniteSets/kuratowski/length.v
index 72ab83b..72ff94a 100644
--- a/FiniteSets/kuratowski/length.v
+++ b/FiniteSets/kuratowski/length.v
@@ -1,8 +1,8 @@
-Require Import HoTT HitTactics.
+Require Import HoTT HitTactics prelude.
 Require Import kuratowski.operations kuratowski.properties kuratowski.kuratowski_sets.
 
 Section Length.
-  Context {A : Type} `{DecidablePaths A} `{Univalence}.
+  Context {A : Type} `{MerelyDecidablePaths A} `{Univalence}.
   
   Definition length : FSet A -> nat.
     simple refine (FSet_cons_rec _ _ _ _ _ _).
@@ -16,11 +16,15 @@ Section Length.
     - intros X a b n.
       simpl.
       simplify_isIn_d.
-      destruct (dec (a = b)) as [Hab | Hab].
-      + rewrite Hab. simplify_isIn_d. reflexivity.
+      destruct (m_dec_path a b) as [Hab | Hab].
+(*      destruct (dec (Trunc (-1) (a = b))) as [Hab | Hab]. *)
+      + strip_truncations.
+        rewrite Hab. simplify_isIn_d. reflexivity.
       + rewrite ?singleton_isIn_d_false; auto.
         ++ simpl. 
            destruct (a ∈_d X), (b ∈_d X) ; reflexivity.
-        ++ intro p. contradiction (Hab p^).
+        ++ intro p. contradiction (Hab (tr p^)).
+        ++ intros p.
+           apply (Hab (tr p)).          
   Defined.
 End Length.
\ No newline at end of file