Let n be given.
Assume Hn: nat_p n.
We will prove (In_rec_i F (ordsucc n) = f n (In_rec_i F n)).
rewrite the current goal using (In_rec_i_eq F nat_primrec_r) (from left to right) at position 1.
We will prove F (ordsucc n) (In_rec_i F) = f n (In_rec_i F n).
We will prove (if ⋃ (ordsucc n) ∈ ordsucc n then f (⋃ (ordsucc n)) (In_rec_i F (⋃ (ordsucc n))) else z) = f n (In_rec_i F n).
rewrite the current goal using (Union_ordsucc_eq n Hn) (from left to right).
We will prove (if n ∈ ordsucc n then f n (In_rec_i F n) else z) = f n (In_rec_i F n).
An exact proof term for the current goal is (If_i_1 (n ∈ ordsucc n) (f n (In_rec_i F n)) z (ordsuccI2 n)).
∎