add theorem to evaluate code_labels on the bootstrapped code

tried running it for a while, but it didn't return: probably the
code_labels_conv is too inefficient at the moment.

will also need to do the same thing on the code for call_repl_step
(currently only doing the code for repl_decs).