rw [BEq.rfl, if_pos rfl]
α : 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 : β
hge : ¬stop < start
this : stop = start
⊢ (if (start == start) = true then pure b
    else
      match start, ⋯ with
      | 0, x => pure b
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f as[i] b
        foldrM.fold f as start i ⋯ __do_lift) =
    pure b
no goals