l:T List, i:
||l||, j:i. last(l_interval(l;j;i)) = l[(i-1)]l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j 
l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)]| Rank | Theorem | Name |
| 4 | l:T List, i:||l||, j:i. last(l_interval(l;j;i)) = l[(i-1)] | [last_l_interval] |
| cites the following: | ||
| 2 | l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j | [length_l_interval] |
| 3 | l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)] | [select_l_interval] |