intro k hk
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n : Nat
⊢ ∀ (k : Nat), k ≤ n → foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
n k : Nat
hk : k ≤ n
⊢ foldM.loop f (n + 1) k = foldM.loop (f ∘ succ) n k