Let x0 of type ι be given.
Let x1 of type ι be given.
Apply If_i_1 with
0 ∈ prim4 0,
x0,
x1,
λ x2 x3 . x2 ∈ UPair x0 x1 leaving 2 subgoals.
The subproof is completed by applying Empty_In_Power with 0.
Apply ReplI with
prim4 (prim4 0),
λ x2 . If_i (0 ∈ x2) x0 x1,
prim4 0.
The subproof is completed by applying Self_In_Power with
prim4 0.