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