(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

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


By: <Unproved Leaf>


Generated subgoals:

None

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

(12steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc