split
case e_a.h
α : 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 : β
⊢ foldrM.fold f as stop start ⋯ b = if stop < start then foldrM.fold f as stop start ⋯ b else pure b
case e_a.h.isTrue
α : 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 : β
h✝ : stop < start
⊢ foldrM.fold f as stop start ⋯ b = foldrM.fold f as stop start ⋯ b

case e_a.h.isFalse
α : 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 : β
h✝ : ¬stop < start
⊢ foldrM.fold f as stop start ⋯ b = pure b