| λ x0 x1 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . cc64c.. (2a987.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2)) (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2))) (2a987.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)) (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3))) |
|