rw [ext_iff, ext_iff (L := L)]
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ -l1 = -l2 → l1 = l2
case mp
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : LawfulLitVar L ν
l1 l2 : L
⊢ toVar (-l1) = toVar (-l2) ∧ polarity (-l1) = polarity (-l2) → toVar l1 = toVar l2 ∧ polarity l1 = polarity l2