IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def exists ==
p:'a

. 
x:'a. (p(x))
is mentioned by
Thm* exists( rep:hone  hbool. type_definition(( b:hbool. b),rep)) | [hone_ty_def] |
In prior sections:
hol bool
Try larger context:
HOLlib
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html