Proofgold Term Root Disambiguation

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

as obj
-

as prop
1dc5a..

theory
HotG

stx
92d75..

address
TMKaD..