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