ext
case pos.h
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ l₁ = l₂
case pos.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ toVar l₁ = toVar l₂

case pos.h.a
l₁ l₂ : ILit
hlit : toVar l₁ = toVar l₂
hpol : polarity l₁ = polarity l₂
⊢ polarity l₁ = polarity l₂