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
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))

By:	SimilarTo: Hyp:-1 ...

None

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