fix bvs_to_chars_def (but compiler proof not updated)

it needed to ensure that the bc values are actually chars
fix compiler proofs for change to bvs_to_chars