Nuprl - Proof: firstn wf 2 1 1 2

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

1. A : Type
2. A List
3. A
4. v : A List
5.

. firstn(n;v)

A List
6. n :

7. 0<n

firstn(n-1;v)

A List

By:	BackThru 5

Generated subgoals:

None

About:

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