simp [foldl, foldlM, Id.run]
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
⊢ foldl f init #[] start stop = init
β : Type u_1
α : Type u_2
f : β → α → β
init : β
start stop : Nat
⊢ (if h : stop = 0 then foldlM.loop f #[] stop ⋯ (stop - start) start init else foldlM.loop f #[] 0 ⋯ 0 start init) =
    init