Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Apply H0 with
λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x1 x2) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x1) = ChurchNums_3x8_to_u24 x2 x1 ⟶ ∀ x3 : ο . x3 leaving 3 subgoals.
Apply H1 with
λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x2) = ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3) x2 ⟶ ∀ x3 : ο . x3 leaving 8 subgoals.
The subproof is completed by applying neq_1_0.
The subproof is completed by applying neq_2_1.
The subproof is completed by applying neq_3_2.
The subproof is completed by applying neq_4_3.
The subproof is completed by applying neq_5_4.
The subproof is completed by applying neq_6_5.
The subproof is completed by applying neq_7_6.
The subproof is completed by applying neq_8_7.
Apply H1 with
λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x2) = ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x4) x2 ⟶ ∀ x3 : ο . x3 leaving 8 subgoals.
The subproof is completed by applying neq_9_8.
The subproof is completed by applying unknownprop_36b306548a78300032c69ad94745ff48aa8608e8a430eca548c144b9c231bda4.
The subproof is completed by applying unknownprop_4ab2aef55b95fb08a1edd1a27d2fff79c4fc64f365bf3591ff27be743265541f.
The subproof is completed by applying unknownprop_dd600363d78f5191d99ddf5f03f668be69bef6f49770dc87b299c981791e709b.
The subproof is completed by applying unknownprop_f4e278a6bf4004a90230a7ce4599c33df3b13afc88036ef1d8ff3a4ef834b193.
The subproof is completed by applying unknownprop_ccf4a5c6b3a6e4954a14109684a2ab83b52a2425e80e3019435c7a784c78b93f.
The subproof is completed by applying unknownprop_9052a17aeb56f0baa5bd35ac678f9db733e32e563a9d0a61b0417ed4592a2293.
The subproof is completed by applying unknownprop_5f312c1824a4beefed581d01c6269bf8f1701f7ed4c65d144b4397173c0fe00c.
Apply H1 with
λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x2) = ChurchNums_3x8_to_u24 (λ x3 x4 x5 : (ι → ι) → ι → ι . x5) x2 ⟶ ∀ x3 : ο . x3 leaving 8 subgoals.
The subproof is completed by applying unknownprop_48ad08e3fcea446c4edb5e27702cf310c322bf29128458b86d14b643f3111333.
The subproof is completed by applying unknownprop_73b9cd20f7c68e88e2ea426419ccd36b4d3b28c76cc72d670d7f8ae953c13bf1.
The subproof is completed by applying unknownprop_fa5098b34d383bdca73a3b8d5098cb7d610846f369975f1b68176e99916d56fc.
The subproof is completed by applying unknownprop_9d0b3600c1008810e1dcd2f5d5b69567f51704fcc4b0f5a23b2c520b26cc4e6b.
The subproof is completed by applying unknownprop_9752f8aae07d669b1096f135020ecbab317a167588504754f80d88b4c92adaa6.
The subproof is completed by applying unknownprop_3d71b5e2b64bf76b23712115efcf8b7f94af2176c7117e30436385825be79563.
The subproof is completed by applying unknownprop_5c1235178ee676092509be5f997555e0c264359c0246b8769d05b358696c7223.