| λ x0 x1 x2 x3 x4 : ι → ι . λ x5 . prim0 (λ x6 . and (SNo x6) (∀ x7 : ο . (∀ x8 . and (SNo x8) (∀ x9 : ο . (∀ x10 . and (SNo x10) (x5 = bbc71.. (x0 x5) (x1 x5) (x2 x5) (x3 x5) (x4 x5) x6 x8 x10) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7)) |
|
| type |
|---|
| (ι → ι) → (ι → ι) → (ι → ι) → (ι → ι) → (ι → ι) → ι → ι |
|
|
|
|
|
|
|
|
|