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

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
x : ν
⊢ toPropForm (mkNeg x) = PropForm.neg (PropForm.var x)
Tactic:
simp [toPropForm]
State after:
no goals