rintro (rfl | rfl)
case mpr
l₁ l₂ : ILit
⊢ l₁ = l₂ ∨ negate l₁ = l₂ → ILit.index l₁ = ILit.index l₂
case mpr.inl
l₁ : ILit
⊢ ILit.index l₁ = ILit.index l₁

case mpr.inr
l₁ : ILit
⊢ ILit.index l₁ = ILit.index (negate l₁)