Theorem | Name |
Thm* 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: |
Thm* a:T, as:T List, i: . i 0  [a / as][i] = a | [select_cons_hd] |
Thm* a:T, as:T List, i: . 0<i  i ||as||  [a / as][i] = as[(i-1)] | [select_cons_tl] |