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

State before:
s : Stack
p : Prog
op : Binop
arg1 arg2 : Nat
⊢ denote (Instr.iBinop op :: p) (arg1 :: arg2 :: s) = denote p (Binop.denote op arg1 arg2 :: s)
Tactic:
rfl
State after:
no goals