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