(17steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: increasing is id 1 1 1 1

1. k : 
2. 0<k
3. f:((k-1)(k-1)). increasing(f;k-1)  (i:(k-1). f(i) = i)
4. f : kk
5. increasing(f;k)
6. k
7. (k-1)
8. f(k-1)<k
  i:(k-1). f(i (k-1)


By: Auto


Generated subgoal:

1 9. i1 : (k-1)
  f(i1 (k-1)

2 steps

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

(17steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc