L:T List. L 
nil 
L = nilL1,L2:T List. L1 L2 
||L1||
||L2||l:T List. ||l|| = 0 
l = nil| Rank | Theorem | Name |
| 3 | L:T List. L nil L = nil | [sublist_nil] |
| cites the following: | ||
| 2 | L1,L2:T List. L1 L2 ||L1||||L2|| | [length_sublist] |
| 0 | l:T List. ||l|| = 0 l = nil | [length_zero] |