Theorem: LeanSAT.LitVar.satisfies_neg (LeanSAT/Data/Cnf.lean)

State before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
⊢ τ ⊨ toPropFun (-l) ↔ (fun M φ => ¬M ⊨ φ) τ (toPropFun l)
Tactic:
simp [satisfies_iff]
State after:
no goals