prove a cheat in bootstrap_lemmas

enabled by the new facts proved about the globals