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