∀ {α : Sort u_1} (n : ℕ) (f : α → Fin n → α) (_x : (_ : α) ×' ℕ),
  Fin.foldl.loop._unary✝ n f _x =
    PSigma.casesOn _x fun x i => if h : i < n then Fin.foldl.loop._unary✝¹ n f ⟨f x ⟨i, h⟩, i + 1⟩ else x