simp [this]
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
hge : ¬stop < start
this : stop = start
⊢ foldrM.fold f as stop start ⋯ b = pure b
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
hge : ¬stop < start
this : stop = start
⊢ foldrM.fold f as start start ⋯ b = pure b