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

By:	UnivCD THEN Compute Replace value k by f(m) in f * i.if f(i)=k f(m) else f(i) fi

1

1. m :  2. k :  3. f : (m+1)(k+1) 4. Inj((m+1); (k+1); f)   (i.if f(i)=k f(m) else f(i) fi)  mk

6 steps

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