From 74eaddee2a0de3e942438a13f7ac7bdd7e485766 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Sun, 24 Sep 2017 18:56:32 +0200
Subject: [PATCH] minor cleanup

---
 FiniteSets/subobjects/b_finite.v | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/FiniteSets/subobjects/b_finite.v b/FiniteSets/subobjects/b_finite.v
index 4be1e0c..a85102a 100644
--- a/FiniteSets/subobjects/b_finite.v
+++ b/FiniteSets/subobjects/b_finite.v
@@ -449,11 +449,7 @@ Section kfin_bfin.
           reflexivity. }
         cbn[Fin].
         etransitivity. apply (notIn_ext_union_singleton b _ HX'Yb).
-        (* TODO: rewrite fw does not work *)
-        apply equiv_path.
-        f_ap.
-        apply (equiv_path _ _)^-1.
-        apply fw.
+        by rewrite ((equiv_path _ _)^-1 fw).
   Defined.
 
   Definition FSet_to_Bfin : forall (X : FSet A), Bfin (map X).