Proofgold Term Root Disambiguation

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

as obj
-

as prop
22358..^{recip_CSNo_invL}

theory
HotG

stx
2ea7a..

address
TMQMa..^{recip_CSNo_invL}