Proofgold Term Root Disambiguation

∀ x0 x1 . not (Inj0 x0 = Inj1 x1)

as obj
-

as prop
efcec..^{Inj0_Inj1_neq}

theory
HF

stx
a6670..

address
TMJxT..^{Inj0_Inj1_neq}