Proofgold Term Root Disambiguation

∀ x0 . HSNo x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nIn (Sing 4) x1

as obj
-

as prop
9cf79..^{octonion_tag_fresh}

theory
HotG

stx
5c6b2..

address
TMafY..^{octonion_tag_fresh}