Proofgold Term Root Disambiguation

∀ x0 x1 . CSNo x0 ⟶ CSNo x1 ⟶ add_HSNo x0 x1 = add_CSNo x0 x1

as obj
-

as prop
b0521..^{add_HSNo_add_CSNo}

theory
HotG

stx
43801..

address
TMUsp..^{add_HSNo_add_CSNo}