Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x3 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Apply H0 with
λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 = (λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x6 x7 x8 : (ι → ι) → ι → ι . x5 x7 x8 x6) x1 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x2 x4) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x2) = ChurchNums_3x8_to_u24 x1 x3 ⟶ ∀ x5 : ο . x5 leaving 3 subgoals.
Apply H2 with
λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) = (λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x6 x7 x8 : (ι → ι) → ι → ι . x5 x7 x8 x6) x4 ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x2 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x2) = ChurchNums_3x8_to_u24 x4 x3 ⟶ ∀ x5 : ο . x5 leaving 3 subgoals.
Assume H4: (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x5.
Apply FalseE with
ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x2 (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x2) = ChurchNums_3x8_to_u24 (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) x3 ⟶ ∀ x4 : ο . x4.
Apply neq_0_1.
Apply H4 with
λ x4 x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x5 (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . x6) (λ x6 : ι → ι . λ x7 . x7) ordsucc 0 = (λ x6 x7 x8 : (ι → ι) → ι → ι . x7) (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . x6) (λ x6 : ι → ι . λ x7 . x7) ordsucc 0.
Let x4 of type ι → ι → ο be given.
Assume H5:
x4 ((λ x5 x6 x7 : (ι → ι) → ι → ι . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) ordsucc 0) ((λ x5 x6 x7 : (ι → ι) → ι → ι . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) (λ x5 : ι → ι . λ x6 . x6) ordsucc 0).
The subproof is completed by applying H5.
Assume H4: (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x6.
Apply FalseE with
ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x2 (λ x4 x5 x6 : (ι → ι) → ι → ι . x4)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x2) = ChurchNums_3x8_to_u24 (λ x4 x5 x6 : (ι → ι) → ι → ι . x5) x3 ⟶ ∀ x4 : ο . x4.
Apply neq_0_1.
Apply H4 with
λ x4 x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x5 (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . x6) ordsucc 0 = (λ x6 x7 x8 : (ι → ι) → ι → ι . x8) (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . x6) ordsucc 0.
Let x4 of type ι → ι → ο be given.
Assume H5:
x4 ((λ x5 x6 x7 : (ι → ι) → ι → ι . x7) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) ordsucc 0) ((λ x5 x6 x7 : (ι → ι) → ι → ι . x7) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . λ x6 . x6) (λ x5 : ι → ι . x5) ordsucc 0).
The subproof is completed by applying H5.
Apply H1 with
λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) = (λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x6 x7 x8 : (ι → ι) → ι → ι . x5 x7 x8 x6) (λ x5 x6 x7 : (ι → ι) → ι → ι . x7) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 x4 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 x4) = ChurchNums_3x8_to_u24 (λ x5 x6 x7 : (ι → ι) → ι → ι . x7) x3 ⟶ ∀ x5 : ο . x5 leaving 8 subgoals.
Apply H3 with
λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) = (λ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x6 x7 x8 : (ι → ι) → ι → ι . x5 x7 x8 x6) (λ x5 x6 x7 : (ι → ι) → ι → ι . x7) ⟶ ChurchNums_3x8_to_u24 (ChurchNums_8x3_to_3_lt7_id_ge7_rot2 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 : (ι → ι) → ι → ι . x5)) (ChurchNums_8_perm_1_2_3_4_5_6_7_0 (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x5)) = ChurchNums_3x8_to_u24 (λ x5 x6 x7 : (ι → ι) → ι → ι . x7) x4 ⟶ ∀ x5 : ο . x5 leaving 8 subgoals.