Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Apply H0 with
λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_8ary_proj_p (ChurchNums_8_perm_3_4_5_6_7_0_1_2 x1) leaving 8 subgoals.
The subproof is completed by applying unknownprop_a820edf1df6b5c92668217259c75ae523851dd9fb028042bb6e14985c16976ff.
The subproof is completed by applying unknownprop_77373a2933cfcb1a37334b719eb77edf1b1748d9da47ba868185fa412d5cdec1.
The subproof is completed by applying unknownprop_f0037219748a33909d912b9fce7a38be396bfa5941888bf986f5ecce1edf8391.
The subproof is completed by applying unknownprop_ec1851fba031ceb8b36005ab5bb38ffa46592f2ab2b842c56650d2f5922b9cc8.
The subproof is completed by applying unknownprop_30cfcf8bf34acb2c5ca68ea0e7be506d609e5867a4d4497397aad7d562af1dab.
The subproof is completed by applying unknownprop_c81ed2e9a17c355a8eba784e3f7c99474839bcd57b59bf65a4f5f4cc009847ea.
The subproof is completed by applying unknownprop_f798ca89c8567ea7da8a78160d7cd47b3d0207ab1034ef92a2ea3a0a4b916fbc.
The subproof is completed by applying unknownprop_d79e0593f17494e6d5530254550ecb02b8a6cc10f6aea3b51be08ce73cab44ac.