cases h
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
no goals