(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

1. T : Type
2. F : k:. (kT)(k+1)T
  n:. Y(F nT


By: NatInd Concl


Generated subgoals:

1   Y(F 0T
PREMISE
2 3. n : 
4. 0<n
5. Y(F (n-1)T
  Y(F nT

4 steps

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

(12steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc