induction n generalizing init with
| zero => exact h0
| succ n IH =>
  dsimp [foldAll]
  rw [Fin.foldAllM_succ' (m:=Id)]
  refine hf ⟨n,n.lt_succ_self⟩ _ ?_
  refine IH _ init h0 ?_
  intro i x H
  exact hf ⟨i.1, .step i.2⟩ x H
n : Nat
α : Type u
motive : Nat → α → Prop
f : Fin n → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive n (foldAll f init)
no goals