(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

1. 'a : S
2. 'a List
3. 'a
4. v : 'a List
5. n:n<||v||  el(n,v) = v[n]
6. n : 
7. n<||v||+1
8. n = 0
  False


By: Analyze 0


Generated subgoals:

None

About:
listintnatural_numberaddless_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