add hol-light/stateful/monadic to build sequence
only translate 8-bit words

This makes word_preludeTheory build faster. I don't think it's used for
anything anyway.
translate new HOL implementation into CakeML

mostly reuse the version in the stateless development, with a couple of
changes due to the presence of axioms, and an alternative workaround for
the MEM problem with first_dup.