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:	x,y:{2..k}. xy xy<k (h:({2..k}).  ({2..k}(g) = {2..k}(h) & h(xy) = 0 & (u:{2..k}. xy<u  h(u) = g(u))) Asserted ... THEN Inst: Thm*  i:{2...}, j:{1...}. j<ij Using:[x | y] ...w

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))	PREMISE
2	3. x,y:{2..k}. 3. xy 3.  3. xy<k 3.  3. (h:({2..k}).  3. ({2..k}(g) = {2..k}(h) 3. (& h(xy) = 0 3. (& (u:{2..k}. xy<u  h(u) = g(u))) 4. x : {2..k} 5. y : {2..k} 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))	2 steps

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