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