match any x (p a) 0 stop with
| true => simp only [ite_true, Bool.true_or]
| false => simp only [ite_false, Bool.false_or]
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ (if any x (p a) 0 stop = true then true else anyPair x p 0 stop) = (any x (p a) 0 stop || anyPair x p 0 stop)
no goals