L1,L2:T List. L1 
L2 
||L1|| = ||L2|| 
L1 = L2a,b:T List. ||a|| = ||b|| (i:
. i<||a|| a[i] = b[i]) a = bk:, f:(k
k). increasing(f;k) (i:k. f(i) = i)| Rank | Theorem | Name |
| 2 | L1,L2:T List. L1 L2 ||L1|| = ||L2|| L1 = L2 | [proper_sublist_length] |
| cites the following: | ||
| 1 | a,b:T List. ||a|| = ||b|| (i:. i<||a|| a[i] = b[i]) a = b | [list_extensionality] |
| 1 | k:, f:(kk). increasing(f;k) (i:k. f(i) = i) | [increasing_is_id] |