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

Elements of union

Browse Source
This commit is contained in:
Niels
2017-05-24 14:52:52 +02:00
parent 826b6ba233
commit 74cd449f7b
1 changed files with 6 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
FiniteSets/properties.v
View File

@@ -429,4 +429,10 @@ hrecursion X; try (intros ; apply set_path2).
rewrite <- Q. rewrite <- Q.
Admitted. Admitted.
Theorem union_isIn (X Y : FSet A) (a : A) : isIn a (U X Y) = orb (isIn a X) (isIn a Y).
Proof.
reflexivity.
Defined.
End properties. End properties.