Proofgold Term Root Disambiguation

∀ x0 x1 . Subq x0 x1 = (binintersect x0 x1 = x0)

as obj
-

as prop
5e05c..^{Subq_binintersection_eq}

theory
HF

stx
cb38c..

address
TMWfU..^{Subq_binintersection_eq}