Proofgold Term Root Disambiguation

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

as obj
7fd81..^proj1

as prop
-

theory
HotG

stx
114a5..

address
TMaSY..^proj1