(3steps total) PrintForm Definitions Lemmas hol num Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hnum ty def
  exists(rep:hnum  hind. type_definition(is_num_rep,rep))
By: HN THEN StrongAuto

Generated subgoal:

1   rep:(hnum  hind). type_definition(hind;hnum;is_num_rep;rep)
2 steps

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

(3steps total) PrintForm Definitions Lemmas hol num Sections HOLlib Doc