IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc ntuple wf1132 1. A : Type
2. n : 3. n1:. n1<n (A^n1) Type
4. n 0
5. n 1
(A^(n-1)) Type
By:
BackThru: Hyp:3
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
n1:
(A^n1) 
Type
0
(A^(n-1)) 
