Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Apply H1 with
λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) x2 x1 = λ x3 x4 . x3) ⟶ ∀ x3 : ο . ((x2 = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) ⟶ x3) ⟶ ((x2 = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5) ⟶ x3) ⟶ ((x2 = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x6) ⟶ x3) ⟶ ((x2 = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x8) ⟶ x3) ⟶ ((x2 = λ x4 x5 x6 : (ι → ι) → ι → ι . x5) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) ⟶ x3) ⟶ ((x2 = λ x4 x5 x6 : (ι → ι) → ι → ι . x5) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5) ⟶ x3) ⟶ ((x2 = λ x4 x5 x6 : (ι → ι) → ι → ι . x5) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x11) ⟶ x3) ⟶ ((x2 = λ x4 x5 x6 : (ι → ι) → ι → ι . x6) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) ⟶ x3) ⟶ ((x2 = λ x4 x5 x6 : (ι → ι) → ι → ι . x6) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x8) ⟶ x3) ⟶ ((x2 = λ x4 x5 x6 : (ι → ι) → ι → ι . x6) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x10) ⟶ x3) ⟶ ((x2 = λ x4 x5 x6 : (ι → ι) → ι → ι . x6) ⟶ (x1 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x11) ⟶ x3) ⟶ x3 leaving 3 subgoals.
Apply H2 with
λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3) x2 = λ x3 x4 . x3) ⟶ ∀ x3 : ο . (((λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ (x2 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) ⟶ x3) ⟶ (((λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ (x2 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5) ⟶ x3) ⟶ (((λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ (x2 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x6) ⟶ x3) ⟶ (((λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ (x2 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x8) ⟶ x3) ⟶ (((λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x5) ⟶ (x2 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) ⟶ x3) ⟶ (((λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x5) ⟶ (x2 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x5) ⟶ x3) ⟶ (((λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x5) ⟶ (x2 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x11) ⟶ x3) ⟶ (((λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x6) ⟶ (x2 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x4) ⟶ x3) ⟶ (((λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x6) ⟶ (x2 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x8) ⟶ x3) ⟶ (((λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x6) ⟶ (x2 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x10) ⟶ x3) ⟶ (((λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x6) ⟶ (x2 = λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x11) ⟶ x3) ⟶ x3 leaving 8 subgoals.
Assume H3:
TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x2 x3 x4 : (ι → ι) → ι → ι . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x2) (λ x2 x3 x4 : (ι → ι) → ι → ι . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 : (ι → ι) → ι → ι . x2) = λ x2 x3 . x2.
Let x2 of type ο be given.
Assume H4: ((λ x3 x4 x5 : (ι → ι) → ι → ι . x3) = λ x3 x4 x5 : (ι → ι) → ι → ι . x3) ⟶ ((λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) = λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) ⟶ x2.
Assume H5: (λ x3 x4 x5 : (ι → ι) → ι → ι . x3) = ... ⟶ ((λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x3) = λ x3 x4 x5 x6 x7 x8 x9 x10 : (ι → ι) → ι → ι . x4) ⟶ x2.