reorganise so good stuff from eval_init_prog proved only once

i.e. separate out the result of applying compiler correctness to the
initial program as a separate theorem.

also, try to prove initial_bc_state_side, but it looks like this is
false because it seems to require the code to be unlabelled.