split up bootstrap evaluation, note problem with label removal

The repl_decs_code_eq theorem was previously not reducing anything
because it wasn't using the bytecode (labels) compset. Now it is
commented out because the call to code_labels is not obviously correct
and won't work anyway since we can't prove good_labels about the result
in compile_repl_decs (only good local labels).

moved labels-related theorems into one theory, and free-vars-related
ones into another, leaving only compiler-evaluation ones in the original
compile_repl_decsTheory.