λ x0 : ι → ι → ο . λ x1 x2 x3 . ∀ x4 : ο . ((x1 = x2 ⟶ ∀ x5 : ο . x5) ⟶ (x1 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x3 ⟶ ∀ x5 : ο . x5) ⟶ not (x0 x1 x2) ⟶ not (x0 x1 x3) ⟶ x0 x2 x3 ⟶ x4) ⟶ x4 |
|
type |
---|
(ι → ι → ο) → ι → ι → ι → ο |
|
|
|
|
|
|
|
|
|