L1,L2:T List. 
null(L2) 
L1 
tl(L2) L1 L2x1,x2:T, L1,L2:T List.
Thm* [x1 / L1]
[x2 / L2] 
x1 = x2 & L1 L2 
[x1 / L1] L2| Rank | Theorem | Name |
| 2 | L1,L2:T List. null(L2) L1 tl(L2) L1 L2 | [sublist_tl] |
| cites the following: | ||
| 1 | x1,x2:T, L1,L2:T List.
Thm* [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2 | [cons_sublist_cons] |