Theorem: LO.Propositional.Superintuitionistic.Formula.neg_inj (Logic/Propositional/Superintuitionistic/Formula.lean)

State before:
α : Type u_1
p q : Formula α
⊢ ~p = ~q ↔ p = q
Tactic:
simp[Tilde.tilde]
State after:
no goals