as:T List, x:T. 0<||as|| 
(x 
tl(as)) (x as)as:A List, n:
(||as||-1). tl(as)[n] = as[(n+1)]l:A List. ||l||
1 ||tl(l)|| = ||l||-1 
| Rank | Theorem | Name |
| 2 | as:T List, x:T. 0<||as|| (x tl(as)) (x as) | [member_tl] |
| cites the following: | ||
| 1 | as:A List, n:(||as||-1). tl(as)[n] = as[(n+1)] | [select_tl] |
| 0 | l:A List. ||l||1 ||tl(l)|| = ||l||-1 | [length_tl] |