Proofgold Term Root Disambiguation

∀ x0 x1 . x0 ⊆ x1 = (binunion x0 x1 = x1)

as obj
-

as prop
c2d39..^{Subq_binunion_eq}

theory
HotG

stx
18c18..

address
TMbui..^{Subq_binunion_eq}