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

State before:
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
l : L
⊢ τ ⊨ toPropFun l ↔ τ (toVar l) = polarity l
Tactic:
dsimp [toPropFun, polarity]
State after:
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
l : L
⊢ (τ ⊨ if polarity l = true then var (toVar l) else (var (toVar l))ᶜ) ↔ τ (toVar l) = polarity l

State before:
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
l : L
⊢ (τ ⊨ if polarity l = true then var (toVar l) else (var (toVar l))ᶜ) ↔ τ (toVar l) = polarity l
Tactic:
aesop
State after:
no goals