rw [Fin.foldAllM_succ' (m:=Id)]
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (Nat.succ n) (Id.run (foldAllM f init))
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (Nat.succ n) (Id.run (foldAllM (f ∘ castSucc) init >>= f { val := n, isLt := (_ : n < Nat.succ n) }))