dan/HITs-Examples
1
0
Fork 0
mirror of https://github.com/nmvdw/HITs-Examples synced 2025-11-03 23:23:51 +01:00
Code Issues Releases Wiki Activity

union idem used for comprehension

Browse Source
This commit is contained in:
Niels van der Weide
2017-10-11 17:11:07 +02:00
parent 0f44ee009b
commit 91899aef6f
1 changed files with 1 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
FiniteSets/kuratowski/operations.v
View File

@@ -54,9 +54,7 @@ Section operations.
- apply nl. - apply nl.
- apply nr. - apply nr.
- intros; simpl. - intros; simpl.
destruct (P x). apply union_idem.
+ apply idem.
+ apply nl.
Defined. Defined.
Definition single_product {A B : Type} (a : A) : FSet B -> FSet (A * B). Definition single_product {A B : Type} (a : A) : FSet B -> FSet (A * B).