Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Apply H0 with
λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 x2 x1 ∈ u24 leaving 3 subgoals.
Apply H1 with
λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3) x2 ∈ u24 leaving 8 subgoals.
The subproof is completed by applying unknownprop_03d05df17e6d0dfb61078a328f1fe2af259d04334e9272f9fef14f1c809e2510.
The subproof is completed by applying unknownprop_c5dd54ff540c2e7015553cdd315dc8688381b6bedc976f1e457626e8ffdaa856.
The subproof is completed by applying unknownprop_3f854ddba19afed67e8e7c926514f1031501db7e4b15f32b9d5f01b0cada5e81.
The subproof is completed by applying unknownprop_2fff731f478df28c1a674607897f3e9c9ecbfa9595ccaf6e18f905ceb0bb25f7.
The subproof is completed by applying unknownprop_e96e9e50864a786761e09a3f4fd2da9f54dbbfeb3b82424aad75a5f448944fc0.
The subproof is completed by applying unknownprop_d89f2f1f31e09b27071252de7f4d74d86cc2d23db60c955d9f549cb676628a10.
The subproof is completed by applying unknownprop_c7d0fe73935e70bba08ba24f03fb35b0b0abe6a7eabe725f9cb73b15035c09a0.
The subproof is completed by applying unknownprop_235e5677af1fafe89d2bb2697544cf837edf8151a25dda26f98acabae5fdae0b.
Apply H1 with
λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x4) x2 ∈ u24 leaving 8 subgoals.
The subproof is completed by applying unknownprop_0f4c81eb7b5e834ce321d2838b45d881fed01d1791f152bb3c26d1422ae365df.
The subproof is completed by applying unknownprop_5787addd81097ac2ea7fd3b1172abfbf1a30344b5fc4ed1cd47246895b0f0015.
The subproof is completed by applying unknownprop_1a4e0d2300206843eb688a99c9a35f2824c67ede9ae4bb884800a018d354645f.
The subproof is completed by applying unknownprop_9f645751091168159704c2a4206614a886f67e90634a40cb2f1007a1ded74870.
The subproof is completed by applying unknownprop_b5a5df59295203515b45ba4025b056a60d583244db6a49137478b750da43f7b3.
The subproof is completed by applying unknownprop_0abeefeb4eb46933d72e1a486c5473e97cee56ce97496efd9a5a68ce64ee26af.
The subproof is completed by applying unknownprop_0cac1a9a7834a54f96522175004935f81e185228129aa1df54e676c23f6ba995.
The subproof is completed by applying unknownprop_d83162a850ff828abdce8caffc89679e0d80feb1430ae78d594baabb506d1d2d.
Apply H1 with
λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x5) x2 ∈ u24 leaving 8 subgoals.
The subproof is completed by applying unknownprop_d993a4c14e25e07f108ccf71eb70196df4d041cab22f0c34487d2c84bc066b21.
The subproof is completed by applying unknownprop_f394ff739bed714709cba792c9696d92733c1ded61ca062a9b12d82ac41ecddb.
The subproof is completed by applying unknownprop_1eec97728e0a8c57720abd635b866ba21b7660f2d2ba57d23e943bb9c927f0f6.
The subproof is completed by applying unknownprop_f65b9a80bd646b6589aee836a42c9ac33767f16f532b283c44342f4b01838f80.
The subproof is completed by applying unknownprop_3eb01877a04a9d2c419449ab855e4f00a8d0766102ebceb0dd5045731d380063.
The subproof is completed by applying unknownprop_64b0a32ee640e413f579b7c26b4a57c295e6dda24858871cd7ae4f4bfcaa9d7b.
The subproof is completed by applying unknownprop_14b4339c93681d1ce5d3452c08084b60a24ed9313066dea7cc1c9e3ed973d5c5.
The subproof is completed by applying unknownprop_cd8132c085d47d8171587cae6c2ea06064bae5af42b68a66661992fe9aa230cd.