l,m:T*. ||l|| = 0 
||m|| > 0 tl((l @ m)) = tl(m) tl_append_back
bs ; a.as' a.(as' @ bs) (recursive)
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
Thm* l,m:T*. ||l|| = 0 ||m|| > 0 hd((l @ m)) = hd(m) hd_append_back
Thm* l,m:T*. ||l|| > 0 hd((l @ m)) = hd(l) hd_append_front
In prior sections: list 1 list 3 autom action sets det automata exponent