rw [Exp.denote_const]
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iConst n] ++ p) s = Prog.denote p (Exp.denote (Exp.const n) :: s)
case const
n : Nat
p : Prog
s : Stack
⊢ Prog.denote ([Instr.iConst n] ++ p) s = Prog.denote p (n :: s)