Nuprl - Proof: firstn all 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: firstn all 1 1 1 1

1. Top List
2. Top
3. v : Top List
4.

. ||v||

(firstn(n;v) ~ v)
5. n :

6. ||v||+1

n
7. 0<n

firstn(n-1;v) ~ v

By:	BackThru 4

Generated subgoals:

None

About:

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