simp [List.drop_eq_nil_of_le, h]
case zero
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i : ℕ
h✝ : i + 0 = n
h : i = n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h✝ (natAdd i x))
no goals