Theorem: Cpdt.Chapter2.TExp.denote_binop (Cpdt/Chapter2/Typed.lean)

State before:
a✝² a✝¹ a✝ : Ty
op : TBinop a✝² a✝¹ a✝
arg1 : TExp a✝²
arg2 : TExp a✝¹
⊢ denote (binop op arg1 arg2) = TBinop.denote op (denote arg1) (denote arg2)
Tactic:
rfl
State after:
no goals