We will prove (In_rec_i F 0 = z).
rewrite the current goal using (In_rec_i_eq F nat_primrec_r) (from left to right).
We will prove F 0 (In_rec_i F) = z.
We will prove (if ⋃ 0 ∈ 0 then f (⋃ 0) (In_rec_i F (⋃ 0)) else z) = z.
An exact proof term for the current goal is (If_i_0 (⋃ 0 ∈ 0) (f (⋃ 0) (In_rec_i F (⋃ 0))) z (EmptyE (⋃ 0))).
∎