. exact Fin.val_eq_of_eq <| h.2 ⟨_, Nat.lt_of_succ_lt_succ hi⟩ ⟨_, Nat.lt_of_succ_lt_succ hj⟩ hxij
case cons.mp.mk.mk.succ.succ
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
n✝¹ : Nat
hi : Nat.succ n✝¹ < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : x[n✝¹] = x[n✝]
⊢ n✝¹ = n✝
no goals