induction e generalizing p s with
| const n =>
  rw [Exp.compile_const]
  rw [Exp.denote_const]
  simp
  rw [Prog.denote_iConst]
| binop b l r lih rih =>
  rw [Exp.compile_binop]
  rw [Exp.denote_binop]
  rw [List.append_assoc (Exp.compile r)]
  rw [List.append_assoc (Exp.compile r)]
  rw [rih]
  rw [List.append_assoc]
  rw [lih]
  simp
  rw [Prog.denote_iBinop_2args]
e : Exp
p : Prog
s : Stack
⊢ Prog.denote (Exp.compile e ++ p) s = Prog.denote p (Exp.denote e :: s)
no goals