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