Proofgold Term Root Disambiguation

∀ x0 x1 x2 . ∀ x3 : ο . (x2 ∈ x0 ⟶ x3) ⟶ (x2 ∈ x1 ⟶ x3) ⟶ x2 ∈ binunion x0 x1 ⟶ x3

as obj
-

as prop
570dd..^binunionE

theory
HotG

stx
8b3c6..

address
TMc2z..^binunionE