Theorem: Cpdt.Chapter2.Exp.denote_binop (Cpdt/Chapter2/Lang.lean)

State before:
op : Binop
l r : Exp
⊢ denote (binop op l r) = Binop.denote op (denote l) (denote r)
Tactic:
rfl
State after:
no goals