Let x0 of type ι be given.

Assume H0: x0 ∈ u6.

Let x1 of type ι be given.

Assume H1: x1 ∈ u6.

Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 (nth_6_tuple x0) (nth_6_tuple x1), λ x2 x3 : ι → ι → ι → ι → ι → ι → ι . Church6_to_u6 (Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 (nth_6_tuple x0) x3) = x1 leaving 2 subgoals.

Apply unknownprop_b152b025e55c2019c513a8a0d54cff455d821e1fcbc18c1cd334196ac6497cb7 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.

Apply unknownprop_4e6c9852b5967105f9e3f4e90af643f42e7ba1f7d7d1afd791d31518051a2a23 with nth_6_tuple x0, nth_6_tuple x1, λ x2 x3 : ι → ι → ι → ι → ι → ι → ι . Church6_to_u6 x3 = x1 leaving 3 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.

Apply unknownprop_72649fc0d609625e17ac53e25cd57a51abe86f395cd11e949eac34127a9e2ea9 with x1.

The subproof is completed by applying H1.

■

Proofgold Proof