Theorem: LeanSAT.Cnf.toPropFun_not (LeanSAT/Data/Cnf.lean)

State before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
c : Clause L
inst✝ : LawfulLitVar L ν
⊢ toPropFun (not c) = (Clause.toPropFun c)ᶜ
Tactic:
ext τ
State after:
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)ᶜ

State before:
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)ᶜ
Tactic:
simp [satisfies_iff, Clause.satisfies_iff, LitVar.satisfies_iff,
  not, Array.mem_def, Bool.eq_not_iff]
State after:
no goals