Proofgold Term Root Disambiguation

λ x0 x1 x2 . ∀ x3 . x3 ∈ RealsStruct_Npos x0 ⟶ RealsStruct_divides x0 x3 x1 ⟶ RealsStruct_divides x0 x3 x2 ⟶ x3 = RealsStruct_one x0

as obj
112ea..^{RealsStruct_coprime}

as prop
-

theory
HotG

stx
0f4f5..

address
TMbzp..^{RealsStruct_coprime}