1. p : 
2. i : 
3. p(i)
4. (least i:. p(i))  {i:(i+1)| p(i) & (j:i. p(j)) }
  (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }

By:	BackThru:  {i:(i+1)| p(i) & (j:i. p(j)) }  {i:| p(i) & (j:. j<i  p(j)) }

1

{i:(i+1)| p(i) & (j:i. p(j)) }  {i:| p(i) & (j:. j<i  p(j)) }

4 steps

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