diff --git a/FiniteSets/subobjects/b_finite.v b/FiniteSets/subobjects/b_finite.v
index 12b0f3a..ca7eda3 100644
--- a/FiniteSets/subobjects/b_finite.v
+++ b/FiniteSets/subobjects/b_finite.v
@@ -411,9 +411,9 @@ Section kfin_bfin.
         destruct (dec (a = b)) as [Hb | Hb]; cbn.
         * refine (Empty_rec _).
           rewrite Hb in Ha.
-          contradiction.            
+          apply (HYb Ha).
         * reflexivity.
-        * destruct (dec (b = b)); [ reflexivity | contradiction ].    
+        * destruct (dec (b = b)) ; [ reflexivity | contradiction ].    
   Defined.    
 
   Theorem bfin_union : @closedUnion A Bfin.