l:T List, i:
||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j 
n:, f:(n
T). ||mklist(n;f)|| = n | Rank | Theorem | Name |
| 2 | l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j | [length_l_interval] |
| cites the following: | ||
| 1 | n:, f:(nT). ||mklist(n;f)|| = n | [mklist_length] |