Proofgold Term Root Disambiguation

∀ x0 x1 x2 . setsum x0 (binunion x1 x2) = binunion (setsum x0 x1) (prim5 x2 Inj1)

as obj
-

as prop
020b9..

theory
HotG

stx
594e8..

address
TMFwM..