Proofgold Term Root Disambiguation

∀ x0 x1 x2 . nIn x2 x1 ⟶ equip x0 x1 ⟶ equip (ordsucc x0) (binunion x1 (Sing x2))

as obj
-

as prop
e8bc0..^{equip_adjoin_ordsucc}

theory
HotG

stx
594e8..

address
TMYgT..^{equip_adjoin_ordsucc}