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