(8steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc ntuple wf 1 1 3
1. A : Type
2. n : 
3. n1:. n1<n  (A^n1)  Type
4. n  0
5. n  1
  A(A^(n-1))  Type
By: Analyze

Generated subgoals:

1   A  Type
Trivial
2   (A^(n-1))  Type
1 step

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

(8steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc