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