1. 
2. 
3. n : 
4. 0<n
  (x,y:. (m:. m+1)(x) = (m:. m+1)(y)    x = y)
  & ((y:. x:. y = (m:. m+1)(x)  )  False)

1

5. y:. x:. y = x+1     False

2 steps

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