(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
T
:Type. Y
(
k
:
. (
k
T
)
(
k
+1)
T
)
T
By:
Analyze
Generated subgoal:
1
1.
T
: Type
Y
(
k
:
. (
k
T
)
(
k
+1)
T
)
T
11
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(12steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
T:Type. Y 
(
k:
. (k
T)(k+1)T)T T:Type. Y (k:. (kT)(k+1)T)T Y (k:. (kT)(k+1)T)T
