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