no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
a : α
⊢ foldrM f init (push arr a) (size (push arr a)) = do
    let init ← f a init
    foldrM f init arr (size arr)
simp [foldrM_eq_reverse_foldlM_data, -size_push]