clean up file
merge lennart's changes (bytes_bits_vector computational and inductive defs); use bytes_bits_vector in proof