(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
1.
T
: Type
Y
(
k
:
. (
k
T
)
(
k
+1)
T
)
T
By:
New:
F
FunExtensionality
Generated subgoals:
1
Y
Void
Void
1
step
2
2.
F
:
k
:
. (
k
T
)
(
k
+1)
T
Y(
F
)
T
9
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(12steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
Y 
(
k:
. (k
T)(k+1)T)T Y (k:. (kT)(k+1)T)T Y VoidVoid
k:. (kT)(k+1)T
Y(F) T
