Proofgold Term Root Disambiguation

∀ x0 x1 . Inj0 x0 = Inj1 x1 ⟶ ∀ x2 : ο . x2

as obj
-

as prop
2b14d..^{Inj0_Inj1_neq}

theory
HotG

stx
114a5..

address
TMNaU..^{Inj0_Inj1_neq}