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