Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ quaternion ⟶ HSNo_proj1 x0 ∈ complex

as obj
-

as prop
32dd4..^{quaternion_p1_complex}

theory
HotG

stx
dd055..

address
TMHC6..^{quaternion_p1_complex}