From 72a44c71f9f8368c53350c02372f9c555bfa539e Mon Sep 17 00:00:00 2001
From: Niels van der Weide <n.vanderweide@science.ru.nl>
Date: Tue, 26 Sep 2017 13:06:47 +0200
Subject: [PATCH] Cleaning in length

---
 FiniteSets/kuratowski/length.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/FiniteSets/kuratowski/length.v b/FiniteSets/kuratowski/length.v
index 539cae0..cd4872c 100644
--- a/FiniteSets/kuratowski/length.v
+++ b/FiniteSets/kuratowski/length.v
@@ -19,7 +19,6 @@ Section length.
       destruct (m_dec_path a b) as [Hab | Hab].
       + strip_truncations.
         rewrite Hab.
-        rewrite ?singleton_isIn_d_aa.
         reflexivity.
       + rewrite ?singleton_isIn_d_false.
         ++ simpl.