split
α : 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
⊢ (if (start + 1 == stop) = true then pure b
    else do
      let __do_lift ← f as[start] b
      foldrM.fold f as stop start ⋯ __do_lift) =
    do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
case 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
h✝ : (start + 1 == stop) = true
⊢ pure b = do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b

case 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
h✝ : ¬(start + 1 == stop) = true
⊢ (do
      let __do_lift ← f as[start] b
      foldrM.fold f as stop start ⋯ __do_lift) =
    do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b