Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ quaternion ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ complex ⟶ ∀ x3 . x3 ∈ complex ⟶ x0 = CSNo_pair x2 x3 ⟶ x1) ⟶ x1

as obj
-

as prop
f4d94..^quaternion_E

theory
HotG

stx
dd055..

address
TMVRq..^quaternion_E