Proofgold Term Root Disambiguation

∀ x0 x1 . Inj1 x0 = Inj1 x1 ⟶ x0 = x1

as obj
-

as prop
3e918..^Inj1_inj

theory
HotG

stx
114a5..

address
TMPRT..^Inj1_inj