∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {motive : β → Prop} {l : List α} {b : β} [inst : Monad m]
  [LawfulMonad m] {f : β → α → m β},
  motive b → (∀ (b : β), motive b → ∀ a ∈ l, SatisfiesM motive (f b a)) → SatisfiesM motive (List.foldlM f b l)