Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Let x1 of type ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p (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 x2 x1) leaving 6 subgoals.
Apply H1 with
λ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p (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 (λ x3 x4 x5 x6 x7 x8 . x3) x2) leaving 6 subgoals.
The subproof is completed by applying unknownprop_043e4b78a0654a6683c9234d3bf7766badd8de7fbbde08ad6810ddd8a4f5acef.
The subproof is completed by applying unknownprop_331adedb7edd49a25927b93fceb0218da7c5b54994dbd262dd5d161f43c67d7a.
The subproof is completed by applying unknownprop_829cc6bcf19535104e1ef14d3c37a121ee539b24777eaff2cd61aead27db443c.
The subproof is completed by applying unknownprop_616c991f45f4fe9d3efb0220d6bfc2b3a9576d02c827cfd1aa156159e180bc78.
The subproof is completed by applying unknownprop_4d8598615c468fd2c2438610c865b021fd567a1a56272aa5746a1a4686cd4fd4.
The subproof is completed by applying unknownprop_c2058c433a08cbd0a9de8592bbafc20a46c3ba8f1b81c7ac182023aff037fe72.
Apply H1 with
λ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p (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 (λ x3 x4 x5 x6 x7 x8 . x4) x2) leaving 6 subgoals.
The subproof is completed by applying unknownprop_043e4b78a0654a6683c9234d3bf7766badd8de7fbbde08ad6810ddd8a4f5acef.
The subproof is completed by applying unknownprop_331adedb7edd49a25927b93fceb0218da7c5b54994dbd262dd5d161f43c67d7a.
The subproof is completed by applying unknownprop_829cc6bcf19535104e1ef14d3c37a121ee539b24777eaff2cd61aead27db443c.
The subproof is completed by applying unknownprop_616c991f45f4fe9d3efb0220d6bfc2b3a9576d02c827cfd1aa156159e180bc78.
The subproof is completed by applying unknownprop_4d8598615c468fd2c2438610c865b021fd567a1a56272aa5746a1a4686cd4fd4.
The subproof is completed by applying unknownprop_c2058c433a08cbd0a9de8592bbafc20a46c3ba8f1b81c7ac182023aff037fe72.
Apply H1 with
λ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p (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 (λ x3 x4 x5 x6 x7 x8 . x5) x2) leaving 6 subgoals.
The subproof is completed by applying unknownprop_043e4b78a0654a6683c9234d3bf7766badd8de7fbbde08ad6810ddd8a4f5acef.
The subproof is completed by applying unknownprop_331adedb7edd49a25927b93fceb0218da7c5b54994dbd262dd5d161f43c67d7a.
The subproof is completed by applying unknownprop_829cc6bcf19535104e1ef14d3c37a121ee539b24777eaff2cd61aead27db443c.
The subproof is completed by applying unknownprop_616c991f45f4fe9d3efb0220d6bfc2b3a9576d02c827cfd1aa156159e180bc78.
The subproof is completed by applying unknownprop_4d8598615c468fd2c2438610c865b021fd567a1a56272aa5746a1a4686cd4fd4.
The subproof is completed by applying unknownprop_c2058c433a08cbd0a9de8592bbafc20a46c3ba8f1b81c7ac182023aff037fe72.
Apply H1 with
λ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p (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 (λ x3 x4 x5 x6 x7 x8 . x6) x2) leaving 6 subgoals.
The subproof is completed by applying unknownprop_043e4b78a0654a6683c9234d3bf7766badd8de7fbbde08ad6810ddd8a4f5acef.
The subproof is completed by applying unknownprop_331adedb7edd49a25927b93fceb0218da7c5b54994dbd262dd5d161f43c67d7a.
The subproof is completed by applying unknownprop_829cc6bcf19535104e1ef14d3c37a121ee539b24777eaff2cd61aead27db443c.
The subproof is completed by applying unknownprop_616c991f45f4fe9d3efb0220d6bfc2b3a9576d02c827cfd1aa156159e180bc78.
The subproof is completed by applying unknownprop_4d8598615c468fd2c2438610c865b021fd567a1a56272aa5746a1a4686cd4fd4.
The subproof is completed by applying unknownprop_c2058c433a08cbd0a9de8592bbafc20a46c3ba8f1b81c7ac182023aff037fe72.
Apply H1 with
λ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p (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 (λ x3 x4 x5 x6 x7 x8 . x7) x2) leaving 6 subgoals.
The subproof is completed by applying unknownprop_043e4b78a0654a6683c9234d3bf7766badd8de7fbbde08ad6810ddd8a4f5acef.
The subproof is completed by applying unknownprop_331adedb7edd49a25927b93fceb0218da7c5b54994dbd262dd5d161f43c67d7a.
The subproof is completed by applying unknownprop_829cc6bcf19535104e1ef14d3c37a121ee539b24777eaff2cd61aead27db443c.
The subproof is completed by applying unknownprop_616c991f45f4fe9d3efb0220d6bfc2b3a9576d02c827cfd1aa156159e180bc78.
The subproof is completed by applying unknownprop_4d8598615c468fd2c2438610c865b021fd567a1a56272aa5746a1a4686cd4fd4.
The subproof is completed by applying unknownprop_c2058c433a08cbd0a9de8592bbafc20a46c3ba8f1b81c7ac182023aff037fe72.
Apply H1 with
λ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p (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 (λ x3 x4 x5 x6 x7 x8 . x8) x2) leaving 6 subgoals.
The subproof is completed by applying unknownprop_043e4b78a0654a6683c9234d3bf7766badd8de7fbbde08ad6810ddd8a4f5acef.
The subproof is completed by applying unknownprop_331adedb7edd49a25927b93fceb0218da7c5b54994dbd262dd5d161f43c67d7a.
The subproof is completed by applying unknownprop_829cc6bcf19535104e1ef14d3c37a121ee539b24777eaff2cd61aead27db443c.
The subproof is completed by applying unknownprop_616c991f45f4fe9d3efb0220d6bfc2b3a9576d02c827cfd1aa156159e180bc78.
The subproof is completed by applying unknownprop_c2058c433a08cbd0a9de8592bbafc20a46c3ba8f1b81c7ac182023aff037fe72.
The subproof is completed by applying unknownprop_4d8598615c468fd2c2438610c865b021fd567a1a56272aa5746a1a4686cd4fd4.