Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x1 : ι → ι → ι → ι → ι → ι → ι . nth_6_tuple (Church6_to_u6 x1) = x1 leaving 6 subgoals.
The subproof is completed by applying unknownprop_5e063b347ef5ac56a92183cc00c589df53087ab1e0b6353a236a973dc2f46966.
The subproof is completed by applying unknownprop_487e017004ecabac0b8e518f0fcaf45b502b6f60f5af04ddefe015bde12eaf50.
The subproof is completed by applying unknownprop_9205282ef77caa3eed787eb4fa460a34079ef649c9bf4aa55e938da8cedd6fa2.
The subproof is completed by applying unknownprop_d77aca9102a0a7995bbfb825c57cbe3520e1f56683b5c476fb6c9389a8c86331.
The subproof is completed by applying unknownprop_d3b792af1adffec16ce4fc340f1433694e312f9a299dc66e7bdd660386d0095e.
The subproof is completed by applying unknownprop_d1ab6c05d827ab2f0497648eeb2e74b0b0260f4e004a74cbc06a5c0a175e4a2a.