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