Let x0 of type CT2 (ι → ι → ι → ι → ι → ι → ι) be given.
Apply H0 with
λ x1 : ((ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . 8915b.. x1 ∈ setprod u6 u6.
Let x1 of type ι → ι → ι → ι → ι → ι → ι be given.
Let x2 of type ι → ι → ι → ι → ι → ι → ι be given.
Apply tuple_2_setprod with
u6,
u6,
Church6_to_u6 x1,
Church6_to_u6 x2 leaving 2 subgoals.
Apply unknownprop_1b4f2955a5c5bc9e0e05efcc9b39724ab6f1c75c28f2f476e2bc7bdba41d9061 with
x1.
The subproof is completed by applying H1.
Apply unknownprop_1b4f2955a5c5bc9e0e05efcc9b39724ab6f1c75c28f2f476e2bc7bdba41d9061 with
x2.
The subproof is completed by applying H2.