PrintForm
Definitions
Lemmas
hol
one
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
one
wd
v
:Unit.
v
=
By:
RewriteOfThm
Thm*
all(
v
:hone. equal(
v
,one_el)) HNC
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
hol
one
Sections
HOLlib
Doc
v:Unit. v = 
v:Unit. v = 
v:hone. equal(v,one_el)) HNC
