L:T List, x:T. 
null(L) 
last([x / L]) = last(L)a:T, as:T List, i:
. 0<i i
||as|| [a / as][i] = as[(i-1)]| Theorem | Name |
| L:T List, x:T. null(L) last([x / L]) = last(L) | [last_cons] |
| cites the following: | |
| a:T, as:T List, i:. 0<i i||as|| [a / as][i] = as[(i-1)] | [select_cons_tl] |