How about trying to prove the following:

mac (compile e ++ x) s = mac x (eval e : s)

You can then just break down your term into pieces, build up the stack
and evaluate it in your prove.