Proofgold Term Root Disambiguation

∀ x0 . finite x0 ⟶ ∀ x1 . finite x1 ⟶ finite (binunion x0 x1)

as obj
-

as prop
3365a..^{binunion_finite}

theory
HotG

stx
2f9e1..

address
TMYXz..^{binunion_finite}