Theorem: Cpdt.Chapter3.Formula.denote_eq (Cpdt/Chapter3/Reflexive.lean)

State before:
l r : Nat
⊢ denote (eq l r) = (l = r)
Tactic:
rfl
State after:
no goals