conv => rhs; dsimp [anyM]; rewrite [dif_pos h]; unfold anyM.loop
α : 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 hj : j + 1 < stop + 1 then
      let_fun this := (_ : 0 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      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
      if 0 < stop + 1 then
        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))
      else pure false) =
    do
    let b ← anyM (p a) x j stop
    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
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : 0 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      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
      if 0 < stop + 1 then
        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))
      else pure false) =
    do
    let b ←
      if hlt : j < stop then
          let_fun this := (_ : j < size x);
          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