Proofgold Term Root Disambiguation

∀ x0 x1 . In x1 (Union x0) ⟶ ∀ x2 : ο . (∀ x3 . In x1 x3 ⟶ In x3 x0 ⟶ x2) ⟶ x2

as obj
-

as prop
2109a..^UnionE2

theory
HF

stx
8a441..

address
TMFkT..^UnionE2