| λ x0 : (ι → ο) → ο . λ x1 : (ι → ι → ο) → ο . λ x2 . λ x3 x4 : ι → ι → ι . and (and (and (x0 (λ x5 . x3 x5 x2 = x5)) (x1 (λ x5 x6 . x3 x5 x6 = x3 x6 x5))) (x0 (λ x5 . x0 (λ x6 . x3 (x4 x5 x6) x6 = x5)))) (x0 (λ x5 . x0 (λ x6 . x4 (x3 x5 x6) x6 = x5))) |
|