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