Let n be given.
We prove the intermediate
claim L1:
∀i ∈ n, f i ∈ ω.
Let i be given.
Assume Hi.
Apply Hf to the current goal.
An exact proof term for the current goal is Hi.
We prove the intermediate
claim L2:
Pi_SNo f n ∈ ω.
We prove the intermediate
claim L3:
f n ∈ ω.
Apply Hf to the current goal.
Let i be given.
rewrite the current goal using
Pi_SNo_S f n Hn (from left to right).
Apply ordsuccE n i Hi to the current goal.
An exact proof term for the current goal is IHn L1 i H1.
rewrite the current goal using H1 (from left to right).
∎