Let x0 of type ι be given.
Apply cases_6 with
x0,
λ x1 . Church6_p (nth_6_tuple x1) leaving 7 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_5e063b347ef5ac56a92183cc00c589df53087ab1e0b6353a236a973dc2f46966 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2.
The subproof is completed by applying unknownprop_331adedb7edd49a25927b93fceb0218da7c5b54994dbd262dd5d161f43c67d7a.
Apply unknownprop_487e017004ecabac0b8e518f0fcaf45b502b6f60f5af04ddefe015bde12eaf50 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2.
The subproof is completed by applying unknownprop_043e4b78a0654a6683c9234d3bf7766badd8de7fbbde08ad6810ddd8a4f5acef.
Apply unknownprop_9205282ef77caa3eed787eb4fa460a34079ef649c9bf4aa55e938da8cedd6fa2 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2.
The subproof is completed by applying unknownprop_616c991f45f4fe9d3efb0220d6bfc2b3a9576d02c827cfd1aa156159e180bc78.
Apply unknownprop_d77aca9102a0a7995bbfb825c57cbe3520e1f56683b5c476fb6c9389a8c86331 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2.
The subproof is completed by applying unknownprop_829cc6bcf19535104e1ef14d3c37a121ee539b24777eaff2cd61aead27db443c.
Apply unknownprop_d3b792af1adffec16ce4fc340f1433694e312f9a299dc66e7bdd660386d0095e with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2.
The subproof is completed by applying unknownprop_c2058c433a08cbd0a9de8592bbafc20a46c3ba8f1b81c7ac182023aff037fe72.
Apply unknownprop_d1ab6c05d827ab2f0497648eeb2e74b0b0260f4e004a74cbc06a5c0a175e4a2a with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2.
The subproof is completed by applying unknownprop_4d8598615c468fd2c2438610c865b021fd567a1a56272aa5746a1a4686cd4fd4.