m,k:, f:((m+1)(k+1)).
  Inj((m+1); (k+1); f)
  
  (i:m. f(i) = k  (Replace value k by f(m) in f)(i) = f(i)  k)

1

1. m :  2. k :  3. f : (m+1)(k+1) 4. Inj((m+1); (k+1); f) 5. i : m 6. f(i) = k   (Replace value k by f(m) in f)(i) = f(i)  k

2 steps

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