Nuprl - Proof: nth tl wf 1 1 2

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

1. A : Type
2. i :

3. 0<i
4. i-1

(

as:A List. nth_tl(i-1;as)

A List)
5. i

0
6. as : A List

nth_tl(i;as)

A List

By:	RW (RecUnfoldC `nth_tl`) 0 THEN SplitOnConclITE

Generated subgoals:

1 7. i0
as A List
Auto

2 7. 0<i
nth_tl(i-1;tl(as)) A List
1 step

About:

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