Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 . Subq x0 x2 ⟶ Subq x1 x3 ⟶ Subq (setsum x0 x1) (setsum x2 x3)

as obj
-

as prop
374e6..^pairSubq

theory
HF

stx
a6670..

address
TMP5C..^pairSubq