simp only [Bool.or_eq_true, beq_iff_eq]
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ (a == b || any x (fun x => a == x) 0 (size x)) = true ↔ a = b ∨ a ∈ x
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ a = b ∨ any x (fun x => a == x) 0 (size x) = true ↔ a = b ∨ a ∈ x