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

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ (mkLit L (toVar l) !polarity l) = -l
Tactic:
ext <;> simp
State after:
no goals