| λ x0 : ((ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (((ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι) → ο . (∀ x2 x3 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2 ⟶ Church6_p x3 ⟶ x1 (λ x4 : (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . x4 x2 x3)) ⟶ x1 x0 |
|