induction l generalizing i j with
| nil => cases hi
| cons a l IH =>
  cases nodup with | cons ha nodup =>
  specialize IH nodup
  cases i <;> cases j <;> dsimp at h
  . rfl
  . exfalso
    suffices a ∈ l from ha a this rfl
    exact List.mem_iff_get.mpr ⟨_, h.symm⟩
  . exfalso
    suffices a ∈ l from ha a this rfl
    exact List.mem_iff_get.mpr ⟨_, h⟩
  . exact congrArg Nat.succ <| IH _ _ h
α : Type u
β : Type v
l : List α
nodup : Nodup l
i j : Nat
hi : i < length l
hj : j < length l
h : l[i] = l[j]
⊢ i = j
no goals