l:T List, i:
||l||, j:i. hd(l_interval(l;j;i)) = l[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. hd(l_interval(l;j;i)) = l[j] | [hd_l_interval] |
| cites the following: | ||
| 3 | l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)] | [select_l_interval] |