1. m : 
2. k : 
3. f : (m+1)(k+1)
4. Inj((m+1); (k+1); f)
5. Surj((m+1); (k+1); f)
  Bij(m; k; Replace value k by f(m) in f)

1	Inj(m; k; Replace value k by f(m) in f)	1 step
2	Surj(m; k; Replace value k by f(m) in f)	6 steps

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