Let x0 of type ι → ι → ι be given.
Let x1 of type ι → (ι → ι → ι) → ι → ι → ι be given.
Apply In_rec_iii_eq with
λ x2 . λ x3 : ι → ι → ι → ι . If_iii (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_4b8d0eae2814d82b838351f4d1fb7ff5105c7a29e53de90feb94a0224c8650a0 with x0, x1.