(6steps total) PrintForm Definitions hol list 2 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hel wd 2 1 1 1
1. 'a : S
2. hlist('a)
3. n : 
4. n+1 = 0
  n+1-1 = n  hnum
By: Analyze THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

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

(6steps total) PrintForm Definitions hol list 2 Sections HOLlib Doc