l1,l2:T List, x:T. l1 
l2 
(x 
l1) (x l2)l1,l2:T List. l1 l2 
||l1||||l2|| & (i:
. i<||l1|| l1[i] = l2[i])| Rank | Theorem | Name |
| 2 | l1,l2:T List, x:T. l1 l2 (x l1) (x l2) | [iseg_member] |
| cites the following: | ||
| 1 | l1,l2:T List. l1 l2 ||l1||||l2|| & (i:. i<||l1|| l1[i] = l2[i]) | [iseg_select] |