Proofgold Term Root Disambiguation

λ x0 . ReplSep x0 (λ x1 . ∃ x2 . Inj0 x2 = x1) Unj

as obj
9c5e4..^proj0

as prop
-

theory
HotG

stx
114a5..

address
TMJAV..^proj0