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
case cons
α : Type u
β : Type v
a : α
l : List α
IH : Nodup l → ∀ (i j : Nat) {hi : i < length l} {hj : j < length l}, l[i] = l[j] → i = j
nodup : Nodup (a :: l)
i j : Nat
hi : i < length (a :: l)
hj : j < length (a :: l)
h : (a :: l)[i] = (a :: l)[j]
⊢ i = j
no goals