conv =>
  lhs; change if any x (p a) 0 stop = true then true else anyPair x p 0 stop
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → Bool
stop : Nat
⊢ (do
      let b ← anyM (p a) x 0 stop
      if b = true then pure true else anyPairM x p 0 stop) =
    (any x (p a) 0 stop || anyPair x p 0 stop)
α : 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)