Thm* y:, as:T*. tl(nth_tl(y;as)) = nth_tl(y+1;as) nth_tl_lem0

Thm* L:T*. 0 < ||L|| L = hd(L).tl(L) hd_tl

In prior sections: list 1