rewrite [dif_neg (fun h' => hj (Nat.lt_of_succ_lt_succ h')), dif_neg hj]
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
⊢ (if hj : j + 1 < stop + 1 then
      let_fun this := (_ : i + 1 < size (cons a x));
      let_fun this_1 := (_ : j + 1 < size (cons a x));
      do
      let __do_lift ← p (cons a x)[i + 1] (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)) (i + 1) (j + 1 + 1)
            (_ : i + 1 < Nat.succ (j + 1))
    else
      if i + 1 < stop + 1 then
        anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1)
          (i + 1 + 2) (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
      else pure false) =
    if hj : j < stop then
      let_fun this := (_ : i < size x);
      let_fun this_1 := (_ : j < size x);
      do
      let __do_lift ← p x[i] x[j]
      if __do_lift = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
    else if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false
α : Type u
β : Type v
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → α → m Bool
stop : Nat
h : stop ≤ size x
i j : Nat
hij : i < j
hj : ¬j < stop
⊢ (if i + 1 < stop + 1 then
      anyPairM.loop (cons a x) p (stop + 1) (_ : Nat.succ stop ≤ Nat.succ (List.length x.data)) (i + 1 + 1) (i + 1 + 2)
        (_ : i + 1 + 1 < Nat.succ (i + 1 + 1))
    else pure false) =
    if i < stop then anyPairM.loop x p stop h (i + 1) (i + 2) (_ : i + 1 < Nat.succ (i + 1)) else pure false