simp [satisfies_iff, Clause.satisfies_iff, LitVar.satisfies_iff,
  not, Array.mem_def, Bool.eq_not_iff]
case a
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
c : Clause L
inst✝ : LawfulLitVar L ν
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (not c) ↔ τ ⊨ (Clause.toPropFun c)ᶜ
no goals