Let x0 of type ι be given.
Apply cases_6 with
x0,
λ x1 . Church6_to_u6 (nth_6_tuple x1) = x1 leaving 7 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_5e063b347ef5ac56a92183cc00c589df53087ab1e0b6353a236a973dc2f46966 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . x2 0 u1 u2 u3 u4 u5 = 0.
Let x1 of type ι → ι → ο be given.
Assume H1:
x1 ((λ x2 x3 x4 x5 x6 x7 . x2) 0 u1 u2 u3 u4 u5) 0.
The subproof is completed by applying H1.
Apply unknownprop_487e017004ecabac0b8e518f0fcaf45b502b6f60f5af04ddefe015bde12eaf50 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . x2 0 u1 u2 u3 u4 u5 = u1.
Let x1 of type ι → ι → ο be given.
Assume H1:
x1 ((λ x2 x3 x4 x5 x6 x7 . x3) 0 u1 u2 u3 u4 u5) u1.
The subproof is completed by applying H1.
Apply unknownprop_9205282ef77caa3eed787eb4fa460a34079ef649c9bf4aa55e938da8cedd6fa2 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . x2 0 u1 u2 u3 u4 u5 = u2.
Let x1 of type ι → ι → ο be given.
Assume H1:
x1 ((λ x2 x3 x4 x5 x6 x7 . x4) 0 u1 u2 u3 u4 u5) u2.
The subproof is completed by applying H1.
Apply unknownprop_d77aca9102a0a7995bbfb825c57cbe3520e1f56683b5c476fb6c9389a8c86331 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . x2 0 u1 u2 u3 u4 u5 = u3.
Let x1 of type ι → ι → ο be given.
Assume H1:
x1 ((λ x2 x3 x4 x5 x6 x7 . x5) 0 u1 u2 u3 u4 u5) u3.
The subproof is completed by applying H1.
Apply unknownprop_d3b792af1adffec16ce4fc340f1433694e312f9a299dc66e7bdd660386d0095e with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . x2 0 u1 u2 u3 u4 u5 = u4.
Let x1 of type ι → ι → ο be given.
Assume H1:
x1 ((λ x2 x3 x4 x5 x6 x7 . x6) 0 u1 u2 u3 u4 u5) u4.
The subproof is completed by applying H1.
Apply unknownprop_d1ab6c05d827ab2f0497648eeb2e74b0b0260f4e004a74cbc06a5c0a175e4a2a with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . x2 0 u1 u2 u3 u4 u5 = u5.
Let x1 of type ι → ι → ο be given.
Assume H1:
x1 ((λ x2 x3 x4 x5 x6 x7 . x7) 0 u1 u2 u3 u4 u5) u5.
The subproof is completed by applying H1.