induction k generalizing a i with
| zero => dsimp [Fin.foldAllM.loop]; cases h; simp only [pure_bind, bind_pure]
| succ k IH =>
  conv =>
    lhs; unfold Fin.foldAllM.loop; dsimp
    rhs; ext; rw [@IH (i+1) _ (i.succ_add (k+1) ▸ h)]
  simp only [← bind_assoc]
  rfl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
k : Nat
h : i + (k + 1) = n + 1
⊢ foldAllM.loop f i a (k + 1) h =
    foldAllM.loop (f ∘ castSucc) i a k (_ : i + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
no goals