apply congrFun
α : 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
⊢ (do
      let b ← anyM (p a) x 0 (size x)
      if b = true then pure true else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) 0 1 Nat.zero_lt_one) =
    do
    let b ← anyM (p a) x 0 stop
    if b = true then pure true
      else anyPairM.loop x p (size x) (_ : Nat.le (size x) (size x)) 0 (0 + 1) (_ : 0 < Nat.succ 0)
case h
α : 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
⊢ bind (anyM (p a) x 0 (size x)) = bind (anyM (p a) x 0 stop)