Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Apply In_rec_i_eq with
λ x2 . λ x3 : ι → ι . If_i (prim3 x2 ∈ x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0,
0,
λ x2 x3 . x3 = x0 leaving 2 subgoals.
The subproof is completed by applying nat_primrec_r with x0, x1.