Thm* l,m:T*. ||l|| = 0 ||m|| > 0 tl((l @ m)) = tl(m) tl_append_back

Thm* l,m:T*. ||l|| > 0 tl((l @ m)) = (tl(l) @ m) tl_append_front

In prior sections: list 1 list 3 autom