Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Let x2 of type ι be given.
Apply In_rec_i_eq with
λ x3 . λ x4 : ι → ι . If_i (prim3 x3 ∈ x3) (x1 (prim3 x3) (x4 (prim3 x3))) x0,
ordsucc x2,
λ x3 x4 . x4 = x1 x2 (In_rec_i (λ x5 . λ x6 : ι → ι . If_i (prim3 x5 ∈ x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x2) leaving 2 subgoals.
The subproof is completed by applying nat_primrec_r with x0, x1.
Apply Union_ordsucc_eq with
x2,
λ x3 x4 . If_i (x4 ∈ ordsucc x2) (x1 x4 (In_rec_i (λ x5 . λ x6 : ι → ι . If_i (prim3 x5 ∈ x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x4)) x0 = x1 x2 (In_rec_i (λ x5 . λ x6 : ι → ι . If_i (prim3 x5 ∈ x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply If_i_1 with
x2 ∈ ordsucc x2,
x1 x2 (In_rec_i (λ x3 . λ x4 : ι → ι . If_i (prim3 x3 ∈ x3) (x1 (prim3 x3) (x4 (prim3 x3))) x0) x2),
x0.
The subproof is completed by applying ordsuccI2 with x2.