apply foldlM_stop
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldl f b as stop stop = b
case hstop
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ stop ≤ as.size