Thm* A:Type, l:A*, n:. 0n n < ||l|| l[n] A
Thm* A:Type, as:A*, i:. nth_tl(i;as) A*
Thm* A:Type, l:A*. ||l||1 hd(l) A
Thm* A:Type, l:A*. tl(l) A*
Thm* i,j:. ij
Thm* i,j:. i < j
Thm* b:. b
About: