Nuprl - Proof: nth tl decomp 4 2 2 2

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

1. T : Type
2. m :

3. 0<m
4.

L:T List. m-1<||L||

(nth_tl(m-1;L) ~ [L[(m-1)] / nth_tl(1+m-1;L)])
5. L : T List
6. m<||L||
7. 0<m
8. 0<1+m
9. nth_tl(m-1;tl(L)) ~ [tl(L)[(m-1)] / nth_tl(1+m-1;tl(L))]

nth_tl(1+m-1;tl(L)) ~ nth_tl(1+m-1;tl(L))

By:

Analyze

Generated subgoals:

None

About:

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