∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop : ℕ} [inst : Monad m] {p : α → Prop}
  {xs : Array { x // p x }} {f : β → { x // p x } → m β} {g : β → α → m β} {x : β},
  (∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x) →
    stop = xs.size → Array.foldlM f x xs 0 stop = Array.foldlM g x xs.unattach 0 stop