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
  g:((k-1)(m-1)). i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi

By:	InstConcl [i.if f(i)=m-1 f(k-1) else f(i) fi]

1	(i.if f(i)=m-1 f(k-1) else f(i) fi)  (k-1)(m-1)	4 steps
2	i:(k-1).    (i.if f(i)=m-1 f(k-1) else f(i) fi)(i) = if f(i)=m-1 f(k-1) else f(i) fi	1 step
3	8. g : (k-1)(m-1)   (i:(k-1). g(i) = if f(i)=m-1 f(k-1) else f(i) fi)  Type	Auto

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