rw [← Bool.bnot_eq] at hpol
case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ polarity (negate l₁) = polarity l₂
case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : (!polarity l₁) = polarity l₂
⊢ polarity (negate l₁) = polarity l₂