'a:S, l:'a List. 
mt(l) 
cons(head(l); tl(l)) = l'a:S. all(
l:hlist('a). implies(not(null(l)),equal(cons(hd(l),tl(l)),l)))| Theorem | Name |
| 'a:S, l:'a List. mt(l) cons(head(l); tl(l)) = l | [cons_char] |
| cites the following: | |
| 'a:S. all(l:hlist('a). implies(not(null(l)),equal(cons(hd(l),tl(l)),l))) | [hcons_char] |