start updating bootstrap_lemmas

move the relevant things to the top of the file, and prove an initial
theorem: COMPILER_RUN_INV_init