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

State before:
⊢ ∀ (f : Formula), denote f → denote (swapper f)
Tactic:
intro f
State after:
f : Formula
⊢ denote f → denote (swapper f)

State before:
f : Formula
⊢ denote f → denote (swapper f)
Tactic:
induction f <;> simp_all
State after:
no goals