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

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
v : ν
⊢ toPropFun (mkLit L v false) = (PropFun.var v)ᶜ
Tactic:
simp [toPropFun]
State after:
no goals