L_1,L_2:T List. L_1 
L_2 
L_1 
L_2k:
. increasing(
i.i;k)l1,l2:T List. l1 l2 
||l1||||l2|| & (i:. i<||l1|| l1[i] = l2[i])l1,l2:T List. l1 l2 ||l1||||l2||| Rank | Theorem | Name |
| 2 | L_1,L_2:T List. L_1 L_2 L_1 L_2 | [iseg_is_sublist] |
| cites the following: | ||
| 0 | k:. increasing(i.i;k) | [id_increasing] |
| 1 | l1,l2:T List. l1 l2 ||l1||||l2|| & (i:. i<||l1|| l1[i] = l2[i]) | [iseg_select] |
| 1 | l1,l2:T List. l1 l2 ||l1||||l2|| | [iseg_length] |