1. k : {2...}
2. g : {2..k}
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))

By:	Decide: xy ...w THENL [Inst: Hyp:3 Using:[x | y] ...;Inst: Hyp:3 Using:[y | x] ...]

1

8. xy 9. h:({2..k}).  9. {2..k}(g) = {2..k}(h) & h(yx) = 0 & (u:{2..k}. yx<u  h(u) = g(u))   h:({2..k}).    {2..k}(g) = {2..k}(h) & h(xy) = 0 & (u:{2..k}. xy<u  h(u) = g(u))

1 step

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