(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
1
1
1.
'a
: S
2.
P
:
'a
(
p
:
'a
.
x
:
'a
. (
p
(
x
)))(
P
) = (
P
=
(
x
:
'a
. true
))
By:
Reduce 0 THEN Simpset [`bequal`] THEN StrongAuto THEN Simp THEN StrongAuto
Generated subgoals:
1
3.
x
:
'a
.
P
(
x
)
P
= (
x
:
'a
. true
)
3
steps
2
3.
P
= (
x
:
'a
. true
)
4.
x
:
'a
P
(
x
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc
(
p:'a
x:'a. (p(x)))(P) = (P =
))
