Theorem: LeanSAT.ILit.index_ne_of_var_ne (LeanSAT/Data/ICnf.lean)

State before:
l₁ l₂ : ILit
⊢ toVar l₁ ≠ toVar l₂ → ILit.index l₁ ≠ ILit.index l₂
Tactic:
intro hne hcon
State after:
l₁ l₂ : ILit
hne : toVar l₁ ≠ toVar l₂
hcon : ILit.index l₁ = ILit.index l₂
⊢ False

State before:
l₁ l₂ : ILit
hne : toVar l₁ ≠ toVar l₂
hcon : ILit.index l₁ = ILit.index l₂
⊢ False
Tactic:
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
State after:
no goals