rw [dif_pos hstop]
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - stop) stop b
    else foldlM.loop f as as.size ⋯ (as.size - stop) stop b) =
    pure b
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldlM.loop f as stop ⋯ (stop - stop) stop b = pure b