Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ι . SNo_ord_seq x0 x1 ⟶ ∀ x2 . SNo x2 ⟶ 2be79.. x0 x1 x2 ⟶ ∀ x3 . SNo x3 ⟶ 2be79.. x0 x1 x3 ⟶ x2 = x3

as obj
-

as prop
5eef1..

theory
HotG

stx
26642..

address
TMScB..