Proofgold Term Root Disambiguation

∀ x0 x1 x2 . In x2 (setprod x0 x1) ⟶ In (proj0 x2) x0

as obj
-

as prop
681fa..^{proj0_setprod}

theory
HF

stx
cbc45..

address
TMY5c..^{proj0_setprod}