| λ x0 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (and (x0 = λ x2 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2 (x0 (λ x3 x4 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)) (x0 (λ x3 x4 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x4))) (64789.. (x0 (λ x1 x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x1)))) (64789.. (x0 (λ x1 x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2))) |
|