Proofgold Term Root Disambiguation

λ x0 x1 . ∀ x2 . x2 ∈ prim3 x1 ⟶ or (ordinal x2) (∃ x3 . and (x3 ∈ x0) (x2 = Sing x3))

as obj
8abcf..^{ExtendedSNoElt_}

as prop
-

theory
HotG

stx
5ed1a..

address
TMHss..^{ExtendedSNoElt_}