'prove' bytes_bits_def_eq (meaning it seems to be true for byte:Z, 0 <= byte < 256. unfortunately not encoded in type, how to automate? TODO