1. k : {2...}
2. g : {2..k}
  x,y:{2..k}.
  xy<k
  
  (h:({2..k}). 
  ({2..k}(g) = {2..k}(h)
  (& h(xy) = 0
  (& (u:{2..k}. xy<u  h(u) = g(u)))

By:	{Without loss of generality, assume xy and observe that y<xy (hence xy {Without loss of generality, assume xy and observe that y<xy (hence  {2..k}) {} SideProof

1

3. x : {2..k} 4. y : {2..k} 5. xy 6. xy<k 7. y<xy   h:({2..k}).    {2..k}(g) = {2..k}(h) & h(xy) = 0 & (u:{2..k}. xy<u  h(u) = g(u))

6 steps

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