split
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (match stop - start with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← f b as[start]
      foldlM.loop f as stop ⋯ i' (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
case h_1
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ : Nat
heq✝ : stop - start = 0
⊢ pure b = do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

case h_2
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq✝ : stop - start = i'✝.succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b as[start]
    foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b