∀ {α : Type u} {m : Type → Type w} [inst : Monad m] (p : α → m Bool) (as : Array α) (stop : ℕ) (h : stop ≤ as.size)
  (j : ℕ),
  Array.anyM.loop p as stop h j =
    if hlt : j < stop then
      have this := ⋯;
      do
      let __do_lift ← p as[j]
      if __do_lift = true then pure true else Array.anyM.loop p as stop h (j + 1)
    else pure false