IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
exponentiation wf nat plus1111 1. n : 2. k : 3. k1:. k1<k (n^k1) 4. k = 0
5. n = 0
n(n^(k-1))
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
k1:
(n^k1) 
k = 0
n
(n^(k-1)) 
