Proofgold Term Root Disambiguation

∀ x0 x1 x2 . x2 ∈ setprod x0 x1 ⟶ proj1 x2 ∈ x1

as obj
-

as prop
afe85..^{proj1_setprod}

theory
HotG

stx
08e38..

address
TMMHA..^{proj1_setprod}