1. k : 
2. 0<k
3. m:. (f:((k-1)m). Inj((k-1); m; f))  k-1m
4. m : 
5. f : km
6. Inj(k; m; f)
7. f(0)  m
  f:((k-1)(m-1)). Inj((k-1); (m-1); f)

By:	Assert (g:((k-1)(m-1)). i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi)

1	g:((k-1)(m-1)). i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi	7 steps
2	8. g:((k-1)(m-1)). i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi   f:((k-1)(m-1)). Inj((k-1); (m-1); f)	27 steps

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