apply Nat.succ.inj
case cons.refine_2
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ i = j
case cons.refine_2.x
α : Type u
β : Type v
a : α
l : List α
IH : (∀ (i j : Nat) (x : i < length l) (x_1 : j < length l), l[i] = l[j] → i = j) → Nodup l
h : ∀ (i j : Nat) (x : i < length (a :: l)) (x_1 : j < length (a :: l)), (a :: l)[i] = (a :: l)[j] → i = j
i j : Nat
hi : i < length l
hj : j < length l
hl : l[i] = l[j]
⊢ Nat.succ i = Nat.succ j