Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_p x1 leaving 4 subgoals.
The subproof is completed by applying unknownprop_331adedb7edd49a25927b93fceb0218da7c5b54994dbd262dd5d161f43c67d7a.
The subproof is completed by applying unknownprop_043e4b78a0654a6683c9234d3bf7766badd8de7fbbde08ad6810ddd8a4f5acef.
The subproof is completed by applying unknownprop_616c991f45f4fe9d3efb0220d6bfc2b3a9576d02c827cfd1aa156159e180bc78.
The subproof is completed by applying unknownprop_829cc6bcf19535104e1ef14d3c37a121ee539b24777eaff2cd61aead27db443c.