Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 . binunion x0 x1 = x2 ⟶ (∀ x5 . x5 ∈ x0 ⟶ nIn x5 x1) ⟶ nat_p x3 ⟶ nat_p x4 ⟶ equip x0 x3 ⟶ equip x2 (add_nat x3 x4) ⟶ equip x1 x4

as obj
-

as prop
8bf56..

theory
HotG

stx
5f786..

address
TMSgb..