Proofgold Term Root Disambiguation

∀ x0 x1 . x1 ∈ x0 ⟶ Inj1 x1 ∈ Inj0 x0

as obj
-

as prop
56537..^Inj0I

theory
HotG

stx
114a5..

address
TMPfd..^Inj0I