(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 1 2
1. T : Type
2. F : k:. (kT)(k+1)T
3. n : 
4. 0<n
5. Y(F)  (n-1)T
  Y(F)  nT
By: FunExtensionality

Generated subgoal:

1 6. x : n
  Y(F,x)  T
3 steps

About:
intnatural_numberaddsubtractless_thanisectapplyfunctionycombuniversemember
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(12steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc