absurd (eq_of_beq heq)
α : 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
heq : (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
α : 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
heq : (start + 1 == stop) = true
⊢ ¬start + 1 = stop