l1,l2:T List. l1 
l2 
||l1||||l2|| & (i:
. i<||l1|| 
l1[i] = l2[i])a:T, as:T List, i:
. i0 [a / as][i] = aa,b:T, l1,l2:T List. [a / l1] [b / l2] a = b & l1 l2a:T, as:T List, i:. 0<i i||as|| [a / as][i] = as[(i-1)]| Theorem | Name |
| l1,l2:T List. l1 l2 ||l1||||l2|| & (i:. i<||l1|| l1[i] = l2[i]) | [iseg_select] |
| cites the following: | |
| a:T, as:T List, i:. i0 [a / as][i] = a | [select_cons_hd] |
| a,b:T, l1,l2:T List. [a / l1] [b / l2] a = b & l1 l2 | [cons_iseg] |
| a:T, as:T List, i:. 0<i i||as|| [a / as][i] = as[(i-1)] | [select_cons_tl] |