exact foldlM_cons (m:=Id) (λ b a => pure (f b a)) init a as
α : Type u
β : Type v
f : β → α → β
init : β
a : α
as : Array α
⊢ foldl f init (cons a as) 0 (size (cons a as)) = foldl f (f init a) as 0 (size as)
no goals