1. k : {2...}
2. g : {2..k}
3. x,y:{2..k}.
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. z : {2..k}
5. prime(z)
6. i : {2..z}
7. j : {2..z}
8. z = ij
9. h:({2..k}). 
9. {2..k}(g) = {2..k}(h) & h(ij) = 0 & (u:{2..k}. ij<u  h(u) = g(u))
  g':({2..k}). 
  {2..k}(g) = {2..k}(g') & g'(z) = 0 & (u:{2..k}. z<u  g'(u) = g(u))

By:	Rewrite by z = ij  {2..k} ...

None

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