Proofgold Term Root Disambiguation

∀ x0 : ι → ι . (∀ x1 . 1eb0a.. x1 ⟶ and (SNo (x0 x1)) (∃ x2 . and (SNo x2) (∃ x4 . and (SNo x4) (∃ x6 . and (SNo x6) (∃ x8 . and (SNo x8) (∃ x10 . and (SNo x10) (∃ x12 . and (SNo x12) (∃ x14 . and (SNo x14) (x1 = bbc71.. (x0 x1) x2 x4 x6 x8 x10 x12 x14))))))))) ⟶ (∀ x1 . 1eb0a.. x1 ⟶ SNo (x0 x1)) ⟶ ∀ x1 x2 x3 x4 x5 x6 x7 x8 . SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ d4639.. x0 (bbc71.. x1 x2 x3 x4 x5 x6 x7 x8) = x2

as obj
-

as prop
33b4a..

theory
HotG

stx
9ceb6..

address
TMLFB..