Who Cites least?
least	Def  least i:. p(i) == if p(0) 0 else (least i:. p(i+1))+1 fi  (recursive)
	Thm*  k:, p:{p:(k)| i:k. p(i) }. (least i:. p(i))  k
	Thm*  p:{p:()| i:. p(i) }. (least i:. p(i))

Syntax:

least i:. p(i)

has structure:

least(i.p(i))

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