specialize h ⟨i+1, Nat.succ_lt_succ hi⟩ ⟨0, x.size.zero_lt_succ⟩ hxi
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ∀ (i j : Fin (size (cons a x))), (cons a x)[↑i] = (cons a x)[↑j] → i = j
hmem : a ∈ x
i : Nat
hi : i < size x
hxi : x[i] = a
⊢ False
case cons.mpr.left
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
hmem : a ∈ x
i : Nat
hi : i < size x
hxi : x[i] = a
h :
  { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ (List.length x.data)) } =
    { val := 0, isLt := (_ : 0 < Nat.succ (size x)) }
⊢ False