Nuprl Basics - Proof: sfa doc find intlist great bound 1 1 2 1 2

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

List
2. u :

3. v :

List
4. w :

||v||. v[i]<w [not for witness]
6.

u<w

{y:

||u.v||. (u.v)[i]<y }

By:	Witness: u+2

Generated subgoal:

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

About:

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