(10steps total) PrintForm Definitions Lemmas hol list 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hel nuprl 1 1
1. 'a : S
2. 'a List
3. u : 'a
4. v : 'a List
5. n:. n<||v||  el(n,v) = v[n]
6. n : 
7. n<||v||+1
  el(n,cons(u; v)) = cons(u; v)[n]
By: RecUnfold `hel` 0 THEN Simp THEN StrongAuto THEN (BifCase THEN HN) THEN Simp
THEN
StrongAuto

Generated subgoals:

1 8. n = 0
  False
1 step
2 8. (n=0) = true
  n<||cons(u; v)||
2 steps
3 8. n = 0
  u = cons(u; v)[n]
1 step
4 8. n = 0
  el(n-1,v) = cons(u; v)[n]
3 steps

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

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