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

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ ⟦toPropForm l⟧ = toPropFun l
Tactic:
dsimp [toPropForm, toPropFun]
State after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ ⟦if polarity l = true then PropForm.var (toVar l) else PropForm.neg (PropForm.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 PropForm.var (toVar l) else PropForm.neg (PropForm.var (toVar l))⟧ =
    if polarity l = true then PropFun.var (toVar l) else (PropFun.var (toVar l))ᶜ
Tactic:
cases polarity l <;> simp
State after:
no goals