From 91899aef6f1add5a39eced36463aa3b17f73a99b Mon Sep 17 00:00:00 2001
From: Niels van der Weide <n.vanderweide@science.ru.nl>
Date: Wed, 11 Oct 2017 17:11:07 +0200
Subject: [PATCH] union idem used for comprehension

---
 FiniteSets/kuratowski/operations.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/FiniteSets/kuratowski/operations.v b/FiniteSets/kuratowski/operations.v
index 493a7ac..dd726d8 100644
--- a/FiniteSets/kuratowski/operations.v
+++ b/FiniteSets/kuratowski/operations.v
@@ -54,9 +54,7 @@ Section operations.
     - apply nl.
     - apply nr.
     - intros; simpl.
-      destruct (P x).
-      + apply idem.
-      + apply nl.
+      apply union_idem.
   Defined.
         
   Definition single_product {A B : Type} (a : A) : FSet B -> FSet (A * B).