Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ octonion ⟶ OSNo_proj1 x0 ∈ quaternion

as obj
-

as prop
ecc21..^{octonion_p1_quaternion}

theory
HotG

stx
dd055..

address
TMYn3..^{octonion_p1_quaternion}