Let n be given.
We prove the intermediate
claim L1:
∀i ∈ n, nat_p (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:
nat_p (Pi_nat f n).
An
exact proof term for the current goal is
Pi_nat_p f n Hn L1.
We prove the intermediate
claim L3:
nat_p (f n).
Apply Hf to the current goal.
Let i be given.
rewrite the current goal using
Pi_nat_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).
∎