Let x0 of type ι → ι be given.
Let x1 of type ι → (ι → ι) → ι → ι be given.
Let x2 of type ι be given.
Apply In_rec_ii_eq with
λ x3 . λ x4 : ι → ι → ι . If_ii (prim3 x3 ∈ x3) (x1 (prim3 x3) (x4 (prim3 x3))) x0,
ordsucc x2,
λ x3 x4 : ι → ι . x4 = x1 x2 (In_rec_ii (λ x5 . λ x6 : ι → ι → ι . If_ii (prim3 x5 ∈ x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x2) leaving 2 subgoals.
The subproof is completed by applying unknownprop_849b5497e74ef64aa6290f57dba7ba4113de693707967a00a0724b0888d48385 with x0, x1.
Apply Union_ordsucc_eq with
x2,
λ x3 x4 . If_ii (x4 ∈ ordsucc x2) (x1 x4 (In_rec_ii (λ x5 . λ x6 : ι → ι → ι . If_ii (prim3 x5 ∈ x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x4)) x0 = x1 x2 (In_rec_ii (λ x5 . λ x6 : ι → ι → ι . If_ii (prim3 x5 ∈ x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply If_ii_1 with
x2 ∈ ordsucc x2,
x1 x2 (In_rec_ii (λ x3 . λ x4 : ι → ι → ι . If_ii (prim3 x3 ∈ x3) (x1 (prim3 x3) (x4 (prim3 x3))) x0) x2),
x0.
The subproof is completed by applying ordsuccI2 with x2.