Sort of an intermediate value thm for continuous fns on ordinals.
Make the zipper example look a little prettier.

- Use Datatype instead of Hol_datatype
- Use [simp] annotations instead of export_rewrites
- Overload zapply to <*>