(9steps total)
PrintForm
Definitions
hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
bnot
ball
1
1
1
1
1.
T
: S
2.
P
:
T
3. XM
4.
(
x
:
T
.
P
(
x
))
5.
x
:
T
P
(
x
)
By:
Decide
P
(
x
) THEN StrongAuto
Generated subgoal:
1
6.
P
(
x
)
P
(
x
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(9steps total)
PrintForm
Definitions
hol
Sections
HOLlib
Doc
(
x:T. P(x))
P(x)
(x:T. P(x))
P(x)P(x)
P(x)
