Theorem: Cpdt.Chapter2.Binop.denote_plus (Cpdt/Chapter2/Lang.lean)

State before:
⊢ denote plus = Nat.add
Tactic:
rfl
State after:
no goals