(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
1
1
1.
'a
: S
2.
P
:
'a
3.
x
:
'a
.
P
(
x
)
4.
x
:
'a
5. True
P
(
x
)
By:
BackThru 3 THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
hol
bool
Sections
HOLlib
Doc