T:Type, l:T List, i:||l||, j:i. last(l_interval(l;j;i)) = l[(i-1)]

By:	Auto THEN Unfold `last` 0 THEN RWO Thm* l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)] 0 THEN Inst Thm* l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j   [T;l;i;j] THEN HypSubst' -1 0

1

1. T : Type 2. l : T List 3. i : ||l|| 4. j : i 5. ||l_interval(l;j;i)|| = i-j     l[(j+i-j-1)] = l[(i-1)]

1 step

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