don't add decode_bc_insts to the_compset

(it causes an error to be printed)
prove compile_prog generates code_labels_ok code

this could have been merged with the main theorem, but is convenient
separate (and was partially lifted from elsewhere).