∀ (P : ℕ → Sort u_1) {n : ℕ} (f : (i : Fin n) → P ↑i → P (↑i + 1)) (i : ℕ) (ubnd : i ≤ n) (a : P i),
  Fin.hIterateFrom P f i ubnd a =
    if g : i < n then Fin.hIterateFrom P f (i + 1) g (f ⟨i, g⟩ a)
    else
      have p := ⋯;
      cast ⋯ a