(5steps total) PrintForm Definitions Lemmas hol one Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hone ty def
  exists(rep:hone  hbool. type_definition((b:hbool. b),rep))
By: HN THEN StrongAuto

Generated subgoal:

1   rep:(Unit). type_definition(;Unit;b:. b;rep)
4 steps

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

(5steps total) PrintForm Definitions Lemmas hol one Sections HOLlib Doc