update the bootstrap evaluation theory

remove the oneshot version.
the new version evaluates repl_decs, and, separately, the code
for making the call to repl_step.

also, exposed the value of the previously existentially quantified
compiler state in compile_repl_decs_thm, to be able to see what state to
use to compile the call.