rw [if_neg (by irreflexivity)]
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if stop < stop then foldrM.fold f as stop stop hstop b else pure b) = pure b
no goals