dsimp [anyPairM]
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
⊢ anyPairM (cons a x) p 0 (stop + 1) = do
    let b ← anyM (p a) x 0 stop
    if b = true then pure true else anyPairM x p 0 stop
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyPairM.loop (cons a x) p (stop + 1) h 0 (0 + 1) (_ : 0 < Nat.succ 0)
    else
      anyPairM.loop (cons a x) p (Nat.succ (size x)) (_ : Nat.le (size (cons a x)) (size (cons a x))) 0 (0 + 1)
        (_ : 0 < Nat.succ 0)) =
    do
    let b ← anyM (p a) x 0 stop
    if b = true then pure true
      else
        if h : stop ≤ size x then anyPairM.loop x p stop h 0 (0 + 1) (_ : 0 < Nat.succ 0)
        else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) 0 (0 + 1) (_ : 0 < Nat.succ 0)