Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . not (inj (prim4 x0) x0 x1)

as obj
-

as prop
2f285..^{form100_63_injCantor}

theory
HotG

stx
adca1..

address
TMas9..^{form100_63_injCantor}