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