1. k : 
2. 0<k
3. p:{p:((k-1))| i:(k-1). p(i) }. 
3. (least i:. p(i))  {i:(k-1)| p(i) & (j:i. p(j)) }
4. p : k
5. i : k
6. p(i)
7. p(0)
8. (least i:. p(i+1))  (k-1)
9. p((least i:. p(i+1))+1)
10. j:(least i:. p(i+1)). p(j+1)
  (least i:. p(i+1))+1  {i:k| p(i) & (j:i. p(j)) }

By:	(least i:. p(i+1))    By BackThru: (k-1)   { for type checking }  THEN Analyze

1

11. (least i:. p(i+1))   12. j : ((least i:. p(i+1))+1)   p(j)

3 steps

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