(6steps total) PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: exponentiation wf nat 1
1. n : 
  k:. (n^k)  
By: CompNatInd Concl

Generated subgoal:

1 2. k : 
3. k1:. k1<k  (n^k1)  
  (n^k)  
4 steps

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

(6steps total) PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc