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