1. p : {p:()| i:. p(i) }
2. (least i:. p(i))  
3. p(least i:. p(i)) & (j:. j<(least i:. p(i))  p(j))  [not for witness]
  j:(least i:. p(i)). p(j)

By:	(least i:. p(i))    By Inclusion 2 { for type checking }  THEN Unhide THEN Analyze3

1

3. p(least i:. p(i)) 4. j:. j<(least i:. p(i))  p(j) 5. (least i:. p(i))     j:(least i:. p(i)). p(j)

1 step

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