Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_to_u6 x1 ∈ u4 leaving 4 subgoals.
The subproof is completed by applying In_0_4.
The subproof is completed by applying In_1_4.
The subproof is completed by applying In_2_4.
The subproof is completed by applying In_3_4.