Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_to_u6 x1 ∈ u6 leaving 6 subgoals.
The subproof is completed by applying In_0_6.
The subproof is completed by applying In_1_6.
The subproof is completed by applying In_2_6.
The subproof is completed by applying In_3_6.
The subproof is completed by applying In_4_6.
The subproof is completed by applying In_5_6.