At: least is least

  k:, p:{p:(k)| i:k. p(i) }, j:(least i:. p(i)). p(j)

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

1

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

2 steps

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