no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : List α
f : α → β → m β
b : β
⊢ List.foldlM (fun y x => f x y) b (reverse (reverse l)) = List.foldlM (fun x y => f y x) b l
simp