Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nIn (Sing 2) x1

as obj
-

as prop
e01e5..^{complex_tag_fresh}

theory
HotG

stx
5ed1a..

address
TMGJY..^{complex_tag_fresh}