constructor
l₁ l₂ : ILit
⊢ ILit.index l₁ = ILit.index l₂ ↔ l₁ = l₂ ∨ negate l₁ = l₂
case mp
l₁ l₂ : ILit
⊢ ILit.index l₁ = ILit.index l₂ → l₁ = l₂ ∨ negate l₁ = l₂

case mpr
l₁ l₂ : ILit
⊢ l₁ = l₂ ∨ negate l₁ = l₂ → ILit.index l₁ = ILit.index l₂