(8steps total) PrintForm Definitions hol list 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hel wf 1 1 1 2
1. 'a : S
2. n : 
3. 0<n
4. l:hlist('a). el(n-1,l)  'a
5. l : hlist('a)
  el(n,l)  'a
By: RecUnfold `hel` 0 THEN Simp THEN CAuto

Generated subgoal:

1 6. n=0
  el(n-1,tl(l))  'a
2 steps

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

(8steps total) PrintForm Definitions hol list 1 Sections HOLlib Doc