rewrite [anyPairM_loop_cons_succ a x p h Nat.zero_lt_one]
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : ¬j < stop
⊢ anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (0 + 1) (0 + 2)
      (_ : 0 + 1 < Nat.succ (0 + 1)) =
    do
    let b ← pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
α : Type u
β : Type v
m : Type → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
j : Nat
hj : ¬j < stop
⊢ anyPairM.loop x p stop h 0 1 Nat.zero_lt_one = do
    let b ← pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one