exact foldlMIdx.loop_cons_succ f a x 0 _ _ b
case h
α : 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
a : α
x : SizedArray α n
b : β (0 + 1)
⊢ foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) b = foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b
no goals