'a:S, l:'a List. ||l|| = 0 
l = nil'a:S. all(
l:hlist('a). equal(equal(length(l),0),equal(l,nil)))| Theorem | Name |
| 'a:S, l:'a List. ||l|| = 0 l = nil | [length_nil_2] |
| cites the following: | |
| 'a:S. all(l:hlist('a). equal(equal(length(l),0),equal(l,nil))) | [hlength_nil_2] |