all
  (P:hnum  hbool. implies
  (P:hnum  hbool. (exists(n:hnum. P(n))
  (P:hnum  hbool. ,exists
  (P:hnum  hbool. ,(n:hnum. and
  (P:hnum  hbool. ,(n:hnum. (P(n)
  (P:hnum  hbool. ,(n:hnum. ,all(m:hnum. implies(lt(m,n),not(P(m))))))))

None

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