Theorem: LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.neg_def (Logic/Propositional/Superintuitionistic/Kripke/Semantics.lean)

State before:
α : Type u_1
inst✝ : Inhabited α
M : Model α
w : M.World
p : Formula α
⊢ Satisfies M w (~p) ↔ ∀ {w' : M.Frame.World}, w ≺ w' → ¬Satisfies M w' p
Tactic:
simp [NegAbbrev.neg]
State after:
no goals