Nuprl - Proof: firstn all 1 1

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

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

. ||v||

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

6. ||v||+1

firstn(n;[u / v]) ~ [u / v]

By:	RecUnfold `firstn` 0 THEN Reduce 0 THEN SplitOnConclITE

Generated subgoals:

1 7. 0<n
[u / firstn(n-1;v)] ~ [u / v]
2 steps

2 7. n0
nil ~ [u / v]
Auto

About:

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

1	7. 0<n [u / firstn(n-1;v)] ~ [u / v]	2 steps
2	7. n0 nil ~ [u / v]	Auto