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

minor cleanup

Browse Source
This commit is contained in:
Dan Frumin
2017-09-24 18:56:32 +02:00
parent bd91e18ad6
commit 74eaddee2a
1 changed files with 1 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
FiniteSets/subobjects/b_finite.v
View File

@@ -449,11 +449,7 @@ Section kfin_bfin.
reflexivity. } reflexivity. }
cbn[Fin]. cbn[Fin].
etransitivity. apply (notIn_ext_union_singleton b _ HX'Yb). etransitivity. apply (notIn_ext_union_singleton b _ HX'Yb).
(* TODO: rewrite fw does not work *) by rewrite ((equiv_path _ _)^-1 fw).
apply equiv_path.
f_ap.
apply (equiv_path _ _)^-1.
apply fw.
Defined. Defined.
Definition FSet_to_Bfin : forall (X : FSet A), Bfin (map X). Definition FSet_to_Bfin : forall (X : FSet A), Bfin (map X).