Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ ∀ x1 . ordinal x1 ⟶ ∀ x2 . x2 ∈ x1 ⟶ add_SNo x0 x2 ∈ add_SNo x0 x1

as obj
-

as prop
0f42b..^{add_SNo_ordinal_InR}

theory
HotG

stx
a3ed2..

address
TMNJw..^{add_SNo_ordinal_InR}