Theorem: LO.Modal.Standard.Formula.degree_not (Logic/Modal/Standard/Formula.lean)

State before:
α : Type u
p : Formula α
⊢ (~p).degree = p.degree
Tactic:
simp [NegAbbrev.neg]
State after:
no goals