l:T*. ||l|| > 0 
hd(rev(l)) = l[(||l||-1)] hd_reverse
"?" ; h.t h
Thm* l:T*. ||l|| > 0 hd(rev(l)) = l[(||l||-1)] hd_reverse
Thm* l:A*, f:(A
B). ||l|| > 0 hd(map(f;l)) = f(hd(l)) hd_map
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
Thm* l:T*. ||l|| > 0 hd(l) = l[0] hd_select
In prior sections: list 3 autom det automata