dsimp [Fin.foldAllM.loop]
case zero
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.zero + 1) = n + 1
⊢ foldAllM.loop f i a (Nat.zero + 1) h =
    foldAllM.loop (f ∘ castSucc) i a Nat.zero (_ : i + Nat.zero = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
case zero
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.zero + 1) = n + 1
⊢ (do
      let __do_lift ← f { val := i, isLt := (_ : i < n + 1) } a
      pure __do_lift) =
    pure a >>= f { val := n, isLt := (_ : n < Nat.succ n) }