intro e p s
⊢ ∀ (e : Exp) (p : Prog) (s : Stack), Prog.denote (Exp.compile e ++ p) s = Prog.denote p (Exp.denote e :: s)
e : Exp
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile e ++ p) s = Prog.denote p (Exp.denote e :: s)