Let x0 of type ι be given.

Assume H0: x0 ∈ u6.

Let x1 of type ι be given.

Assume H1: x1 ∈ u6.

Let x2 of type (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο be given.

Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 (nth_6_tuple x0) (nth_6_tuple x1), λ x3 x4 : ι → ι → ι → ι → ι → ι → ι . x2 x4 x3.

Apply unknownprop_87b44ea852a703abaf8b1ee45427f8c0cbd069f7b68987ed3e5257508f1d4189 with nth_6_tuple x0, nth_6_tuple x1 leaving 2 subgoals.

Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x0.

The subproof is completed by applying H0.

Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x1.

The subproof is completed by applying H1.

■

Proofgold Proof