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

Thm* t:T. rev([t]) = [t] reverse_cons_nil

Thm* l:T*. ||rev(l)|| = ||l|| length_reverse

In prior sections: list 1