Proofgold Term Root Disambiguation

∀ x0 . CSNo x0 ⟶ (x0 = 0 ⟶ ∀ x1 : ο . x1) ⟶ mul_CSNo x0 (recip_CSNo x0) = 1

as obj
-

as prop
c71b1..^{recip_CSNo_invR}

theory
HotG

stx
2ea7a..

address
TMRTM..^{recip_CSNo_invR}