intro ha b hb heq
case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
⊢ ¬a ∈ as → ∀ (a_2 : α), a_2 ∈ as → a_2 ≠ a
case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
ha : ¬a ∈ as
b : α
hb : b ∈ as
heq : b = a
⊢ False