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.