Thm* A:Type, as:A*, i:. nth_tl(i;as) A*
Thm* A:Type, l:A*. tl(l) A*
Thm* i,j:. ij
Thm* i,j:. i < j
Thm* b:. b
About: