At: least satisfies2

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

By:	SimilarTo: Thm*  p:{p:()| i:. p(i) }.  Thm*  (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }

1

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

1 step

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