rcases mkPos_or_mkNeg l₁ with (hl₁ | hl₁)
<;> rw [hl₁] at hcon
<;> rcases mkPos_or_mkNeg l₂ with (hl₂ | hl₂)
<;> rw [hl₂] at hcon
<;> simp at hcon
<;> contradiction
l₁ l₂ : ILit
hne : toVar l₁ ≠ toVar l₂
hcon : ILit.index l₁ = ILit.index l₂
⊢ False
no goals