'a:S, h:'a, t:'a List, h':'a, t':'a List.
Thm* cons(h; t) = cons(h'; t')
h = h' & t = t''a:S, h:'a, t:'a List, h':'a, t':'a List.
Thm* cons(h; t) = cons(h'; t')
h = h' & t = t'| Rank | Theorem | Name |
| 2 | 'a:S, h:'a, t:'a List, h':'a, t':'a List.
Thm* cons(h; t) = cons(h'; t') h = h' & t = t' | [cons_11_2] |
| cites the following: | ||
| 1 | 'a:S, h:'a, t:'a List, h':'a, t':'a List.
Thm* cons(h; t) = cons(h'; t') h = h' & t = t' | [cons_11] |