Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x1 leaving 4 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.