Let x0 of type ι → ι → ι be given.
Let x1 of type ι → (ι → ι → ι) → ι → ι → ι be given.
Let x2 of type ι be given.
Apply In_rec_iii_eq with
λ x3 . λ x4 : ι → ι → ι → ι . If_iii (prim3 x3 ∈ x3) (x1 (prim3 x3) (x4 (prim3 x3))) x0,
ordsucc x2,
λ x3 x4 : ι → ι → ι . x4 = x1 x2 (In_rec_iii (λ x5 . λ x6 : ι → ι → ι → ι . If_iii (prim3 x5 ∈ x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x2) leaving 2 subgoals.
The subproof is completed by applying unknownprop_4b8d0eae2814d82b838351f4d1fb7ff5105c7a29e53de90feb94a0224c8650a0 with x0, x1.
Apply Union_ordsucc_eq with
x2,
λ x3 x4 . If_iii (x4 ∈ ordsucc x2) (x1 x4 (In_rec_iii (λ x5 . λ x6 : ι → ι → ι → ι . If_iii (prim3 x5 ∈ x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x4)) x0 = x1 x2 (In_rec_iii (λ x5 . λ x6 : ι → ι → ι → ι . If_iii (prim3 x5 ∈ x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply If_iii_1 with
x2 ∈ ordsucc x2,
x1 x2 (In_rec_iii (λ x3 . λ x4 : ι → ι → ι → ι . If_iii (prim3 x3 ∈ x3) (x1 (prim3 x3) (x4 (prim3 x3))) x0) x2),
x0.
The subproof is completed by applying ordsuccI2 with x2.