Let f and n be given.

Assume Hn.

We will prove Pi_SNo f (ordsucc n) = Pi_SNo f n * f n.

An exact proof term for the current goal is nat_primrec_S 1 (λi r ⇒ r * f i) n Hn.

∎