more hacking on bootstrap_lemmas

collect all the stuff about the semantics of the last 3 (fake)
declarations into a single specific theorem

start working on the "step preserves inv" theorem
define and starting verifying a special compiler for the repl call

the problem is we want to run the code for calling repl_step multiple
times, so it should already be there in the bytecode machine at the
start, but the compiler's invariants are set up assuming you are about
to install the new code. this can all be worked around if we know the
code doesn't contain any labels, which should be true for the code for
calling repl_step, but the normal compiler has error handlers and other
things involving labels. so define a special compiler for code that is
known to terminate succesfully and not introduce any bindings and not
contain any functions (hence no labels), which skips the code
environment generation and the error handling.