(46steps total) PrintForm Definitions hol num Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: num iso 2 1 2 1 1 1 2 1
1. y:. x:. y = x+1
  False
By: ((DTerm 0 1) THEN (Analyze 1)) THEN StrongAuto
THEN
Try (Complete (Unfold `label` 0))

Generated subgoals:

None

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

(46steps total) PrintForm Definitions hol num Sections HOLlib Doc