Proofgold Term Root Disambiguation

∀ x0 x1 . x0 ⊆ x1 ⟶ binintersect x0 x1 = x0

as obj
-

as prop
ec1cc..^{binintersect_Subq_eq_1}

theory
HotG

stx
18c18..

address
TMGUR..^{binintersect_Subq_eq_1}