Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ octonion ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ quaternion ⟶ ∀ x3 . x3 ∈ quaternion ⟶ x0 = HSNo_pair x2 x3 ⟶ x1) ⟶ x1

as obj
-

as prop
eacc7..^octonion_E

theory
HotG

stx
dd055..

address
TMYor..^octonion_E