update bc_num and num_bc with new instructions
shorten and update proof of bc_next_append_code

collapse almost-identical tactics for several cases into a single tactic
for all of them