1. p : {p:()| i:. p(i) }
  j:(least i:. p(i)). p(j)

By:	Use:[p] Inst:  Thm*  p:{p:()| i:. p(i) }.  Thm*  (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }

1

2. (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }   j:(least i:. p(i)). p(j)

3 steps

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