ext
case neg.h
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ negate l₁ = l₂
case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ toVar (negate l₁) = toVar l₂

case neg.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : ¬polarity l₁ = polarity l₂
⊢ polarity (negate l₁) = polarity l₂