(12steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
ycomb
typing
demo
1
2
2
1.
T
: Type
2.
F
:
k
:
. (
k
T
)
(
k
+1)
T
3.
n
:
. Y(
F
)
n
T
Y(
F
)
T
By:
With (
0
T
) FunExtensionality THENW BackThru: Hyp:3
Generated subgoal:
1
4.
x
:
Y(
F
,
x
)
T
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(12steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
k:
. (
T)
n:
Y(F) 
