some cleanup of compiler/proofs

superficial pass, up to but not including toBytecodeProofsScript.sml