case succ n h_ind =>
  rw [ofFn_succ']; dsimp [List.foldl]; rw [h_ind, Fin.foldAll_succ]; rfl
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
no goals