Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ SNoLt 0 x0 ⟶ and (SNo (recip_SNo_pos x0)) (mul_SNo x0 (recip_SNo_pos x0) = 1)

as obj
-

as prop
78526..^{recip_SNo_pos_prop1}

theory
HotG

stx
0e794..

address
TMLgy..^{recip_SNo_pos_prop1}