Proofgold Term Root Disambiguation

∀ x0 . SNo x0 ⟶ mul_SNo x0 1 = x0

as obj
-

as prop
5477a..^mul_SNo_oneR

theory
HotG

stx
0d8c8..

address
TMPJY..^mul_SNo_oneR