Theorem: Cpdt.Chapter2.TInstr.denote_iBinop (Cpdt/Chapter2/Typed.lean)

State before:
a✝³ a✝² a✝¹ : Ty
op : TBinop a✝³ a✝² a✝¹
arg1 : Ty.denote a✝³
arg2 : Ty.denote a✝²
a✝ : List Ty
s' : VStack a✝
⊢ denote (iBinop op) (arg1, arg2, s') = (TBinop.denote op arg1 arg2, s')
Tactic:
rfl
State after:
no goals