Let x0 of type CT2 (ι → ι → ι → ι → ι → ι → ι) be given.
Apply H0 with
λ x1 : ((ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . 4aafd.. (8915b.. x1) = x1.
Let x1 of type ι → ι → ι → ι → ι → ι → ι be given.
Let x2 of type ι → ι → ι → ι → ι → ι → ι be given.
Apply tuple_2_0_eq with
Church6_to_u6 x1,
Church6_to_u6 x2,
λ x3 x4 . (λ x5 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x5 (nth_6_tuple x4) (nth_6_tuple (ap (lam 2 (λ x6 . If_i (x6 = 0) (Church6_to_u6 x1) (Church6_to_u6 x2))) u1))) = λ x5 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x5 x1 x2.
Apply tuple_2_1_eq with
Church6_to_u6 x1,
Church6_to_u6 x2,
λ x3 x4 . (λ x5 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x5 (nth_6_tuple (Church6_to_u6 x1)) (nth_6_tuple x4)) = λ x5 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x5 x1 x2.
Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with
x1,
λ x3 x4 : ι → ι → ι → ι → ι → ι → ι . (λ x5 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x5 x4 (nth_6_tuple (Church6_to_u6 x2))) = λ x5 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x5 x1 x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with
x2,
λ x3 x4 : ι → ι → ι → ι → ι → ι → ι . (λ x5 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x5 x1 x4) = λ x5 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x5 x1 x2 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x3 of type (CT2 (ι → ι → ι → ι → ι → ι → ι)) → (CT2 (ι → ι → ι → ι → ι → ι → ι)) → ο be given.
Assume H3: x3 (λ x4 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x4 x1 x2) (λ x4 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x4 x1 x2).
The subproof is completed by applying H3.