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

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

1

if f(i)=k f(m) else f(i) fi = f(i)  k

1 step

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