Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_to_u17 x1 ∈ u17 leaving 17 subgoals.
The subproof is completed by applying unknownprop_9851dfe301262128a9dc5def6f083cbb499c4d0eace7612e5dc050c4fe5ba3c7.
The subproof is completed by applying unknownprop_4f0f2f2c8505addb4aa66d1187553d1cf0a291464cc87b78a3faaf7ae73ed155.
The subproof is completed by applying unknownprop_fcb0372c2816a1d869a174f57c9ee90635b20300695b8cc5b4a5ca8436427e30.
The subproof is completed by applying unknownprop_515e04c9d20f4760fa1f9ec9f7d43a79e2cf83cd96ac9929a00f63e10a33bee6.
The subproof is completed by applying unknownprop_8bfb0eb80a8f5f9fa400351ad533eb8f6abcbab81f79751d9b99dc5c5b198b37.
The subproof is completed by applying unknownprop_add6307eacf71a9b26cddaf6256b63e565e929785d0ee0946ee6b253d6c3852e.
The subproof is completed by applying unknownprop_e8645556daad09b81c208e8cbf014ff23194c321a76d028c3b35a1714720baab.
The subproof is completed by applying unknownprop_97cf1bf10df747733c6e7166825443492e8a9bbd5381654e4874ef5f3ceacd0a.
The subproof is completed by applying unknownprop_6e6799a9f21ccdffe58af218db8306610bd1441f3fa0fcc3f6eaa957ce165f57.
The subproof is completed by applying unknownprop_abbef1301044c000653f42960a8047881f2ef656bd9cecef0ae9b764b6c0784f.
The subproof is completed by applying unknownprop_7af243686256d97349e2c2a55c958e2d435fe9a5e016344b19465fce23ad5676.
The subproof is completed by applying unknownprop_fde6379bebd0b99b66d966901300c529916d83c8c1f209841f486bb2568cf012.
The subproof is completed by applying unknownprop_b7a4a37161804b376f25028de76b0714142123cbd842ba90c86afe8baa6a8a9e.
The subproof is completed by applying unknownprop_ee249701bfbf4a0ddc5825c1bc6fff36b37e7d1af2b7d307fdfcf229c66eb3d7.
The subproof is completed by applying unknownprop_19ecd6ac8599e49ad47f95e5b1703b05d2332ac49ec04a48785748b0d8a5094a.
The subproof is completed by applying unknownprop_35f4d337254964d13bfee3413f1b56f908aee5828cc15d13f416e7a488640c53.
The subproof is completed by applying unknownprop_a76efb72f36a26d5f27a9b9224b42b8be1785c9e1b5b0390f7ccb72d2b130266.