Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ quaternion ⟶ ∀ x1 . x1 ∈ quaternion ⟶ OSNo_proj1 (HSNo_pair x0 x1) = x1

as obj
-

as prop
f4be4..^{octonion_p1_eq}

theory
HotG

stx
dd055..

address
TMNqE..^{octonion_p1_eq}