1. Tail recursive versions of the list processing functions from
2. Extensional equality proofs that these variants are
(extensionally) equivalent to their non-tail-recursive
1. Written in one sitting, feel free to refactor
2. The proofs below also work on non-publicly exported
definitions. This could be due to a bug, and will need to be
moved elsewhere if it's fixed.