'a:S. True & (h:'a, t:'a List. True)'a:S. and(null(nil),all(
h:'a. all(t:hlist('a). not(null(cons(h,t))))))| Theorem | Name |
| 'a:S. True & (h:'a, t:'a List. True) | [null_char] |
| cites the following: | |
| 'a:S. and(null(nil),all(h:'a. all(t:hlist('a). not(null(cons(h,t)))))) | [hnull_char] |