Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies.neg_def (Logic/Propositional/Superintuitionistic/Kripke/Classical.lean)

State before:
α : Type u_1
inst✝ : Inhabited α
V : ClassicalValuation α
p : Formula α
⊢ V ⊧ ~p ↔ ¬V ⊧ p
Tactic:
simp only [NegAbbrev.neg, imp_def, bot_def]
State after:
no goals