Nuprl Basics - Proof: sfa doc find intlist great bound 1 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

List
2. u :

3. v :

List
4. {y:

||v||. v[i]<y }

{y:

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

By:	New:w Analyze-1

Generated subgoal:

1 4. w :
5. i:||v||. v[i]<w [not for witness]
{y:| i:||u.v||. (u.v)[i]<y }
13 steps

About:

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