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