unfold foldlMIdx
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ foldlMIdx f init empty = pure init
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ foldlMIdx.loop f empty 0 (_ : 0 ≤ 0) init = pure init