Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x1 leaving 8 subgoals.
The subproof is completed by applying unknownprop_e6619adff47bbbf90a12e5475c1b155ebb1e2991a2d17411fd40e422e21ff562.
The subproof is completed by applying unknownprop_93ed18843f4a06fdb1762e5b7fc89edc8da24a5d38de418508f9aca3fe120f8f.
The subproof is completed by applying unknownprop_233906471c2a36e258793125988364b5b4be5e26b5df943569d8a15ce4c97b59.
The subproof is completed by applying unknownprop_497df65ae9348f62989259dc92fffa35cd477d735ac36c17e9f5dc63bcd5da15.
The subproof is completed by applying unknownprop_aeac4ee3d08fd60f864a3d40a6422b2070323f5bdb4e126705e59ff4ccf8fa26.
The subproof is completed by applying unknownprop_398a24facf4ebb42cf838f8cb0f1d64c4d83d480adfd36e0fa2e0b1bde52df48.
The subproof is completed by applying unknownprop_8422ea19f7ca229a936fab0e3a1aadb25110b62375b34ff2715e426e6903f401.
The subproof is completed by applying unknownprop_d792dc995f6520052dfc965493173e3531c29f8140df360fa3c27b7268ed80b5.