Theorem: Cpdt.Chapter2.Prog.denote_iConst (Cpdt/Chapter2/Lang.lean)

State before:
s : Stack
p : Prog
n : Nat
⊢ denote (Instr.iConst n :: p) s = denote p (n :: s)
Tactic:
rfl
State after:
no goals