prove cheat in compile_append_out

the statement doesn't talk about code_labels_ok directly, but hopefully
what is does say will be enough to prove that.