simp [satisfies_iff, τ.set_get]
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
⊢ PropAssignment.set τ (toVar l) (polarity l) ⊨ toPropFun l
no goals