Theorem: LeanSAT.Model.PropFun.not_satisfiable_iff_eq_bot (LeanSAT/Model/PropFun.lean)

State before:
ν : Type u_1
F : PropFun ν
⊢ ¬satisfiable F ↔ F = ⊥
Tactic:
simp [satisfiable]
State after:
ν : Type u_1
F : PropFun ν
⊢ (∀ (x : PropAssignment ν), ¬x ⊨ F) ↔ F = ⊥

State before:
ν : Type u_1
F : PropFun ν
⊢ (∀ (x : PropAssignment ν), ¬x ⊨ F) ↔ F = ⊥
Tactic:
aesop
State after:
no goals