| λ x0 : ((ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι) → ι → ι → ι → ι → ι → ι → ι . lam 2 (λ x1 . If_i (x1 = 0) (Church6_to_u6 (x0 (λ x2 x3 : ι → ι → ι → ι → ι → ι → ι . x2))) (Church6_to_u6 (x0 (λ x2 x3 : ι → ι → ι → ι → ι → ι → ι . x3)))) |
|