move l2n dropWhile stuff to HOL
prove a deref_byte_thm

showing abs_ml_inv preserved by what is likely to happen when doing
deref byte. not sure it's right yet though.