if hj : j < stop then
  simp only [dif_pos (Nat.succ_lt_succ hj), dif_pos hj]
  simp only [getElem_cons_zero, getElem_cons_succ, bind_assoc]
  apply bind_congr; intro b
  match b with
  | true => simp only [ite_true, pure_bind]
  | false =>
    simp only [ite_false]
    rewrite [anyPairM_loop_cons_zero a x p h (j+1)]
    conv => lhs; lhs; dsimp [anyM]; rw [dif_pos h]
else
  simp only [dif_neg (fun h' => hj (Nat.lt_of_succ_lt_succ h')), dif_neg hj]
  rewrite [anyPairM_loop_cons_succ a x p h Nat.zero_lt_one]
  simp only [pure_bind, ite_false]
α : 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
⊢ (if h_1 : j + 1 < stop + 1 then do
      let __do_lift ← p (cons a x)[0] (cons a x)[j + 1]
      if __do_lift = true then pure true
        else
          anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) 0 (j + 1 + 1)
            (_ : 0 < Nat.succ (j + 1))
    else
      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 ←
      if h_1 : j < stop then do
          let __do_lift ← p a x[j]
          if __do_lift = true then pure true else anyM.loop (p a) x stop h (j + 1)
        else pure false
    if b = true then pure true else anyPairM.loop x p stop h 0 1 Nat.zero_lt_one
no goals