(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. 'a : S
2. l : hlist('a)
3. n : 
4. n+1 = 0
  el(n+1-1,tl(l)) = el(n,tl(l))
By: Analyze THEN Simp THEN StrongAuto THEN Analyze THEN Simp THEN StrongAuto

Generated subgoal:

1   n+1-1 = n  hnum
1 step

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

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