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

State before:
⊢ denote times = Nat.mul
Tactic:
rfl
State after:
no goals