'a:S, t:'a List, h:'a. 
nil = cons(h; t)'a:S. all(
t:hlist('a). all(h:'a. not(equal(nil,cons(h,t)))))| Theorem | Name |
| 'a:S, t:'a List, h:'a. nil = cons(h; t) | [not_nil_cons] |
| cites the following: | |
| 'a:S. all(t:hlist('a). all(h:'a. not(equal(nil,cons(h,t))))) | [hnot_nil_cons] |