intro b
case h
α : 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
⊢ ∀ (a_1 : Bool),
    (if a_1 = 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))) =
      if a_1 = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)
case h
α : 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
b : Bool
⊢ (if b = 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))) =
    if b = true then pure true else anyPairM.loop x p stop h i (j + 1) (_ : i < Nat.succ j)