Theorem: LeanSAT.LitVar.toPropFun_neg (LeanSAT/Data/Cnf.lean)

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ toPropFun (-l) = (toPropFun l)ᶜ
Tactic:
dsimp [toPropFun]
State after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ (if polarity (-l) = true then PropFun.var (toVar (-l)) else (PropFun.var (toVar (-l)))ᶜ) =
    (if polarity l = true then PropFun.var (toVar l) else (PropFun.var (toVar l))ᶜ)ᶜ

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ (if polarity (-l) = true then PropFun.var (toVar (-l)) else (PropFun.var (toVar (-l)))ᶜ) =
    (if polarity l = true then PropFun.var (toVar l) else (PropFun.var (toVar l))ᶜ)ᶜ
Tactic:
aesop
State after:
no goals