prove compile_top_append_code, use in repl_correct

to prove three cheats