Proofgold Term Root Disambiguation

∀ x0 . In 0 x0 ⟶ ∀ x1 x2 . Subq x1 x2 ⟶ Subq (setexp x0 x1) (setexp x0 x2)

as obj
-

as prop
49ee1..^{setexp_0_dom_mon}

theory
HF

stx
89549..

address
TMWad..^{setexp_0_dom_mon}