1. k : 
2. 0<k
3. m:. (f:((k-1)m). Inj((k-1); m; f))  k-1m
4. m : 
5. f : km
6. a1,a2:k. f(a1) = f(a2)  a1 = a2
7. f(0)  m
8. g : (k-1)(m-1)
9. i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi
10. a1 : (k-1)
11. g(a1) = if f(a1)=m-1 f(k-1) else f(a1) fi
12. a2 : (k-1)
13. g(a2) = if f(a2)=m-1 f(k-1) else f(a2) fi
14. f(a1) = m-1
15. f(a2) = m-1
  f(k-1) = f(a2)  (m-1)  a1 = a2

1	16. f(k-1) = f(a2)  (m-1)   a1 = a2	1 step
2	f(k-1)  (m-1)	4 steps

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