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

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ - -l = l
Tactic:
rw [ext_iff]
State after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ toVar (- -l) = toVar l ∧ polarity (- -l) = polarity l

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l : L
⊢ toVar (- -l) = toVar l ∧ polarity (- -l) = polarity l
Tactic:
simp
State after:
no goals