| ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9 ∈ x8 ⟶ ∀ x10 : ι → ο . x10 x0 ⟶ x10 x1 ⟶ x10 x2 ⟶ x10 x3 ⟶ x10 x4 ⟶ x10 x5 ⟶ x10 x6 ⟶ x10 x7 ⟶ x10 x9) ⟶ (x0 = x1 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x2 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x2 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x3 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x3 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x3 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x4 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x5 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x6 ⟶ ∀ x9 : ο . x9) ⟶ (x0 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x1 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x2 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x3 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x4 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x5 = x7 ⟶ ∀ x9 : ο . x9) ⟶ (x6 = x7 ⟶ ∀ x9 : ο . x9) ⟶ not (TwoRamseyProp_atleastp 3 4 x8) |
|