Thm* l:T*. ||l|| > 0 hd(rev(l)) = l[(||l||-1)] hd_reverse

Thm* l:T*. ||l|| > 0 hd(l) = l[0] hd_select

In prior sections: list 1 list 3 autom det automata