1. P : Prop
2. i:. P(i)
3. p : 
4. i:. p(i)  P(i)
5. (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }
6. u : {i:| p(i) & (j:. j<i  p(j)) }
  u  {i:| P(i) & (j:. j<i  P(j)) }

1

6. u :  7. p(u) & (j:. j<u  p(j))   P(u) & (j:. j<u  P(j))

1 step

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