(2steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
heta
ax
'b
,
'a
:S. all(
t
:
'a
'b
. equal((
x
:
'a
.
t
(
x
)),
t
))
By:
Simpsetp [`hol_to_nuprl`] THEN StrongAuto
Generated subgoal:
1
1.
'b
: S
2.
'a
: S
3.
t
:
'a
'b
(
x
:
'a
.
t
(
x
)) =
t
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
'b,'a:S. all(
t:'a 
'b. equal((x:'a. t(x)),t)) 'b,'a:S. all(t:'a 'b. equal((x:'a. t(x)),t))'b
(x:'a. t(x)) = t
