Let x0 of type ι be given.
Let x1 of type (CT2 (ι → ι → ι → ι → ι → ι → ι)) → ο be given.
Assume H1:
∀ x2 x3 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2 ⟶ Church6_p x3 ⟶ x1 (λ x4 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x4 x2 x3).
Apply H1 with
nth_6_tuple (ap x0 0),
nth_6_tuple (ap x0 u1) leaving 2 subgoals.
Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with
ap x0 0.
Apply ap0_Sigma with
u6,
λ x2 . u6,
x0.
The subproof is completed by applying H0.
Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with
ap x0 u1.
Apply ap1_Sigma with
u6,
λ x2 . u6,
x0.
The subproof is completed by applying H0.