(19steps total) PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc find intlist great bound 1 1 2 1 2 1 a

1.  List
2. u : 
3. v :  List
4. w : 
5. i:||v||. v[i]<w
6. u<w
7. i : ||u.v||
  (u.v)[i]<u+2


By: Decide: 0<i


Generated subgoals:

1 8. 0<i
  (u.v)[i]<u+2

2 steps
2 8. 0<i
  (u.v)[i]<u+2

1 step

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

(19steps total) PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Doc