simp only [satisfies_iff]
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
⊢ τ ⊨ toPropFun l → (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x p) (toPropFun l) → l = mkLit L x !p
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
l : L
x : ν
p : Bool
⊢ τ (toVar l) = polarity l → ¬PropAssignment.set τ x p (toVar l) = polarity l → l = mkLit L x !p