Nuprl - Proof: firstn append 2 1

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

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

L2:Top List, n:

(||v||+1). firstn(n;v @ L2) ~ firstn(n;v)
5. L2 : Top List
6. n :

(||v||+1+1)
7. 0<n

firstn(n-1;v @ L2) ~ firstn(n-1;v)

By:	BackThru 4

Generated subgoals:

None

About:

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