dsimp [toPropFun, polarity]
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
l : L
⊢ τ ⊨ toPropFun l ↔ τ (toVar l) = polarity l
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