l1,l2:T List. nil = (l1 @ l2) 
l1 = nil & l2 = nill1,l2:T List. (l1 @ l2) = nil l1 = nil & l2 = nil| Theorem | Name |
| Thm* l1,l2:T List. nil = (l1 @ l2) l1 = nil & l2 = nil | [nil_is_append] |
| cites | |
| Thm* l1,l2:T List. (l1 @ l2) = nil l1 = nil & l2 = nil | [append_is_nil] |