(6steps total) PrintForm Definitions mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bijection restriction 1
1. k : 
2. f : kk
3. 0<k
4. Bij(k; k; f)
5. f(k-1) = k-1
  f  (k-1)(k-1)
By: ExtWith [`z'] [kk]

Generated subgoal:

1 6. z : (k-1)
  f(z)  (k-1)
2 steps

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

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