apply h.1
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ False
case cons.mp.mk.mk.zero.succ.h
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
h : ¬a ∈ x ∧ ∀ (i j : Fin (size x)), x[↑i] = x[↑j] → i = j
hi : Nat.zero < size (cons a x)
n✝ : Nat
hj : Nat.succ n✝ < size (cons a x)
hxij : a = x[n✝]
⊢ a ∈ x