simp only [← bind_assoc]
case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
k : Nat
IH :
  ∀ {i : Nat} {a : α} {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) }
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (f { val := i, isLt := (_ : i < n + 1) } a >>= fun x =>
      foldAllM.loop (f ∘ castSucc) (i + 1) x k (_ : i + 1 + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }) =
    foldAllM.loop (f ∘ castSucc) i a (Nat.succ k) (_ : i + Nat.succ k = n) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) }
case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
k : Nat
IH :
  ∀ {i : Nat} {a : α} {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) }
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (do
        let x ← f { val := i, isLt := (_ : i < n + 1) } a
        foldAllM.loop (f ∘ castSucc) (i + 1) x k (_ : i + 1 + k = n)) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) } =
    foldAllM.loop (f ∘ castSucc) i a (Nat.succ k) (_ : i + Nat.succ k = n) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) }