progress on bootstrap_lemmas, now using compile_special
prove COMPILER_RUN_INV_repl_step

with a cheat about nothing in the globals of the bootstrap_bc_state
being NONE; the invariants in the early languages aren't really set up
to prove this semantically. if we can't/don't want to prove this by
evaluation, then they should probably be strengthened (I'm thinking of
global_env_inv).
Updated intlang pretty print
prove globals don't change in compile_special_thm

but requires assumption that the incoming bytecode state's globals are
all SOME
prove that compile_top preserves all SOME globals

in the case of a successful declaration. I am hoping this will be enough
to chain back the bootstrap bytecode state back to the initial state,
and thereby show that all the globals at the end are SOME.

this turned out to only require a very simple property of
evaluate_prompt_i1.
add trace to make labels_computeLib quiet
prove a cheat in bootstrap_lemmas

enabled by the new facts proved about the globals
Merge remote-tracking branch 'origin/master' into Word8Array