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

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