cases heq
case h.mpr
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
ha : ¬a ∈ as
b : α
hb : b ∈ as
heq : b = a
⊢ False
case h.mpr.refl
α : Type u
inst✝ : DecidableEq α
as : Array α
a : α
ha : ¬a ∈ as
hb : a ∈ as
⊢ False