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