congr
α : 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
⊢ (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 e_a
α : 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
⊢ (fun __do_lift => foldrM.fold f as stop start ⋯ __do_lift) = fun 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