hol
one
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
equal(one_el,select(
x
:hone. t))
[hone_def]
cites the following:
Thm*
a
:Unit.
a
=
[unit_triviality]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
one
Sections
HOLlib
Doc
x:hone. t))
a:Unit. a = 
x:hone. t))a:Unit. a =