(7steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hforall
def
'a
:S. equal(all,
P
:
'a
hbool. equal(
P
,
x
:
'a
. t))
By:
Simpset [`hol_to_nuprl`] THEN StrongAuto THEN Simp THEN StrongAuto
Generated subgoal:
1
1.
'a
: S
(
p
:
'a
.
x
:
'a
. (
p
(
x
))) = (
P
:
'a
.
P
=
(
x
:
'a
. true
))
6
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
'a:S. equal(all,
P:'a 
hbool. equal(P,x:'a. t)) 'a:S. equal(all,P:'a hbool. equal(P,x:'a. t)) (p:'a
. 
x:'a. (p(x))) = (P:'a. P = (x:'a. true
))
