Let n be given.

We will prove nat_primrec 1 (λ_ r ⇒ n * r) 0 = 1.

An exact proof term for the current goal is nat_primrec_0 1 (λ_ r ⇒ n * r).

∎