x,y:T, L:T List.
Thm* (x
L) 
(y L) x = y 
x before y L y before x La:T, as:T List, i:
. i
0 [a / as][i] = aa:T, as:T List, i:. 0<i i||as|| [a / as][i] = as[(i-1)]| Theorem | Name |
| x,y:T, L:T List.
Thm* (x L) (y L) x = y x before y L y before x L | [l_tricotomy] |
| cites the following: | |
| a:T, as:T List, i:. i0 [a / as][i] = a | [select_cons_hd] |
| a:T, as:T List, i:. 0<i i||as|| [a / as][i] = as[(i-1)] | [select_cons_tl] |