move some lemmas from bootstrapScript.sml to compiler/proofs