rw [dif_neg (by irreflexivity)]
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if hlt : stop < stop then
      match stop - stop with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b as[stop]
        foldlM.loop f as stop ⋯ i' (stop + 1) __do_lift
    else pure b) =
    pure b
no goals