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

State before:
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ τ ⊨ φᶜ ↔ (fun M φ => ¬M ⊨ φ) τ φ
Tactic:
simp [sEntails, satisfies, HasCompl.compl]
State after:
no goals