r:
, L:Top List. ||nth_tl(r;L)|| = if r<
||L||
||L||-r else 0 fil:A List. ||l||
1 
||tl(l)|| = ||l||-1 
| Theorem | Name |
| r:, L:Top List. ||nth_tl(r;L)|| = if r<||L|| ||L||-r else 0 fi | [general_length_nth_tl] |
| cites the following: | |
| l:A List. ||l||1 ||tl(l)|| = ||l||-1 | [length_tl] |