PrintForm
Definitions
Lemmas
hol
combin
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
i
thm
'a
:S,
x
:
'a
.
x
=
x
By:
RewriteOfThm
Thm*
'a
:S. all(
x
:
'a
. equal(i(
x
),
x
)) (SimpsetC [`hol_to_nuprl`])
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
hol
combin
Sections
HOLlib
Doc
'a:S, x:'a. x = x 'a:S, x:'a. x = x'a:S. all(
x:'a. equal(i(x),x)) (SimpsetC [`hol_to_nuprl`])
