Proofgold Term Root Disambiguation

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

as obj
-

as prop
e6aa6..^{adjoin_finite}

theory
HotG

stx
2f9e1..

address
TMNv6..^{adjoin_finite}