simp only [Array.foldrM]
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldrM f b as stop stop = pure b
α : Type u_1
β : Type u_3
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 if stop < stop then foldrM.fold f as stop stop h b else pure b
    else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b) =
    pure b