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

State before:
l r : Formula
⊢ denote (and l r) = (denote l ∧ denote r)
Tactic:
rfl
State after:
no goals