prove theorem about compile_fake_exp, with no cheats

but still unsure of statement.
also make a start on trying to state things about compile_dec.