From c6f756a856768e1217a1f12f7a385948f9bacc9b Mon Sep 17 00:00:00 2001 From: Niels van der Weide Date: Wed, 11 Oct 2017 17:45:37 +0200 Subject: [PATCH] Clarified proof of notIn_ext_union_singleton --- FiniteSets/subobjects/b_finite.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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.