| ∀ x0 x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (∀ x4 : ο . ((x0 = λ x6 x7 x8 : (ι → ι) → ι → ι . x6) ⟶ (x2 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x10) ⟶ x4) ⟶ ((x0 = λ x6 x7 x8 : (ι → ι) → ι → ι . x7) ⟶ (x2 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x7) ⟶ x4) ⟶ ((x0 = λ x6 x7 x8 : (ι → ι) → ι → ι . x7) ⟶ (x2 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x13) ⟶ x4) ⟶ ((x0 = λ x6 x7 x8 : (ι → ι) → ι → ι . x8) ⟶ (x2 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x10) ⟶ x4) ⟶ x4) ⟶ (∀ x4 : ο . ((x1 = λ x6 x7 x8 : (ι → ι) → ι → ι . x6) ⟶ (x3 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x10) ⟶ x4) ⟶ ((x1 = λ x6 x7 x8 : (ι → ι) → ι → ι . x7) ⟶ (x3 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x7) ⟶ x4) ⟶ ((x1 = λ x6 x7 x8 : (ι → ι) → ι → ι . x7) ⟶ (x3 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x13) ⟶ x4) ⟶ ((x1 = λ x6 x7 x8 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x10) ⟶ x4) ⟶ x4) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x9) x0 x2 = λ x5 x6 . x5) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x5 x6 x7 : (ι → ι) → ι → ι . x5) (λ x5 x6 x7 x8 x9 x10 x11 x12 : (ι → ι) → ι → ι . x9) x1 x3 = λ x5 x6 . x5) ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x8) x0 x2 ⟶ ChurchNums_3x8_neq (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) (λ x4 x5 x6 x7 x8 x9 x10 x11 : (ι → ι) → ι → ι . x8) x1 x3 ⟶ ChurchNums_3x8_neq x0 x2 x1 x3 ⟶ False |
|