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