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

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

State before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : LawfulLitVar L ν
inst✝ : DecidableEq ν
l : L
⊢ PropFun.semVars (if polarity l = true then PropFun.var (toVar l) else (PropFun.var (toVar l))ᶜ) = {toVar l}
Tactic:
cases polarity l <;> simp
State after:
no goals